package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.17.0.tar.gz
sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250
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