package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.15.1.tar.gz
sha256=513e953b7183d478acb75fd6e80e4dc32ac1a918cf4343ac31a859cfb4e9aad2
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