package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.15.2.tar.gz
sha256=13a67c0a4559ae22e9765c8fdb88957b16c2b335a2d5f47e4d6d9b4b8b299926
doc/ltac_plugin/Ltac_plugin/G_rewrite/index.html
Module Ltac_plugin.G_rewrite
Source
Source
type glob_constr_with_bindings_sign =
Geninterp.interp_sign * Genintern.glob_constr_and_expr Tactypes.with_bindings
Source
val pr_glob_constr_with_bindings_sign :
Environ.env ->
Evd.evar_map ->
'a ->
'b ->
'c ->
glob_constr_with_bindings_sign ->
Pp.t
Source
val pr_glob_constr_with_bindings :
Environ.env ->
Evd.evar_map ->
'a ->
'b ->
'c ->
glob_constr_with_bindings ->
Pp.t
Source
val pr_constr_expr_with_bindings :
'a ->
'b ->
('a -> 'b -> Constrexpr.constr_expr -> 'c) ->
'd ->
'e ->
constr_expr_with_bindings ->
'c
Source
val glob_glob_constr_with_bindings :
Tacintern.glob_sign ->
(Constrexpr.constr_expr * Constrexpr.constr_expr Tactypes.bindings) ->
Genintern.glob_constr_and_expr
* Genintern.glob_constr_and_expr Tactypes.bindings
Source
val subst_glob_constr_with_bindings :
Mod_subst.substitution ->
Genintern.glob_constr_and_expr Tactypes.with_bindings ->
Genintern.glob_constr_and_expr Tactypes.with_bindings
Source
val wit_glob_constr_with_bindings :
(Constrexpr.constr_expr Tactypes.with_bindings,
Genintern.glob_constr_and_expr Tactypes.with_bindings,
glob_constr_with_bindings_sign)
Genarg.genarg_type
Source
type glob_strategy =
(Genintern.glob_constr_and_expr, Tacexpr.glob_red_expr) Rewrite.strategy_ast
Source
val interp_strategy :
Tacinterp.interp_sign ->
'a ->
'b ->
(Genintern.glob_constr_and_expr, Tacexpr.glob_red_expr) Rewrite.strategy_ast ->
Rewrite.strategy
Source
val pr_raw_strategy :
Environ.env ->
Evd.evar_map ->
(Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t) ->
'a ->
raw_strategy ->
Pp.t
Source
val pr_glob_strategy :
Environ.env ->
Evd.evar_map ->
(Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr -> Pp.t) ->
'a ->
glob_strategy ->
Pp.t
Source
val rewstrategy :
(Constrexpr.constr_expr, Genredexpr.raw_red_expr) Rewrite.strategy_ast
Pcoq.Entry.t
Source
val cl_rewrite_clause_db :
Tacinterp.interp_sign ->
string ->
Names.Id.t option ->
unit Proofview.tactic
Source
val clsubstitute :
bool ->
(Tacinterp.interp_sign
* (Genintern.glob_constr_and_expr
* Genintern.glob_constr_and_expr Tactypes.bindings)) ->
unit Proofview.tactic
Source
val declare_relation :
Rewrite.rewrite_attributes ->
Constrexpr.constr_expr ->
?binders:Constrexpr.local_binder_expr list ->
Constrexpr.constr_expr ->
Names.Id.t CAst.t ->
Constrexpr.constr_expr option ->
Constrexpr.constr_expr option ->
Constrexpr.constr_expr option ->
unit
Source
val add_setoid :
Rewrite.rewrite_attributes ->
Constrexpr.local_binder_expr list ->
Constrexpr.constr_expr ->
Constrexpr.constr_expr ->
Constrexpr.constr_expr ->
Names.Id.t CAst.t ->
unit
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>