package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
doc/ssreflect_plugin/Ssreflect_plugin/Ssrparser/index.html
Module Ssreflect_plugin.SsrparserSource
Source
val pr_ssrtacarg :
Environ.env ->
Evd.evar_map ->
'a ->
'b ->
(Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> 'c) ->
'cSource
val pr_ssrtclarg :
Environ.env ->
Evd.evar_map ->
'a ->
'b ->
(Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> 'c -> 'd) ->
'c ->
'dSource
val add_genarg :
string ->
(Environ.env -> Evd.evar_map -> 'a -> Pp.t) ->
'a Genarg.uniform_genarg_typeSource
type ssrarg =
ssrfwdview
* (ssreqid
* (Ssrmatching_plugin.Ssrmatching.cpattern Ssrast.ssragens
* Ssrast.ssripats))Source
val wit_ssrintrosarg :
(Ltac_plugin.Tacexpr.raw_tactic_expr * Ssrast.ssripats,
Ltac_plugin.Tacexpr.glob_tactic_expr * Ssrast.ssripats,
Geninterp.Val.t * Ssrast.ssripats)
Genarg.genarg_typeSource
val wit_ssrcongrarg :
((int * Ssrast.ssrterm)
* Ssrmatching_plugin.Ssrmatching.cpattern Ssrast.ssragens)
Genarg.uniform_genarg_typeSource
val wit_ssrsetfwd :
((Ssrast.ssrfwdfmt
* (Ssrmatching_plugin.Ssrmatching.cpattern * Ssrast.ast_closure_term option))
* Ssrast.ssrdocc)
Genarg.uniform_genarg_typeSource
val wit_ssrwlogfwd :
(Ssrast.clause list * (Ssrast.ssrfwdfmt * Ssrast.ast_closure_term))
Genarg.uniform_genarg_typeSource
val wit_ssrfixfwd :
(Names.Id.t * (Ssrast.ssrfwdfmt * Ssrast.ast_closure_term))
Genarg.uniform_genarg_typeSource
val wit_ssrdgens_tl :
Ssrmatching_plugin.Ssrmatching.cpattern Ssrast.ssragens
Genarg.uniform_genarg_type