package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.0.tar.gz
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b
doc/funind_plugin/Funind_plugin/Glob_termops/index.html
Module Funind_plugin.Glob_termopsSource
Source
val mkGLambda :
(Names.Name.t * Glob_term.glob_constr * Glob_term.glob_constr) ->
Glob_term.glob_constrSource
val mkGProd :
(Names.Name.t * Glob_term.glob_constr * Glob_term.glob_constr) ->
Glob_term.glob_constrSource
val mkGLetIn :
(Names.Name.t
* Glob_term.glob_constr
* Glob_term.glob_constr option
* Glob_term.glob_constr) ->
Glob_term.glob_constrSource
val mkGCases :
(Glob_term.glob_constr option
* Glob_term.tomatch_tuples
* Glob_term.cases_clauses) ->
Glob_term.glob_constrSource
val glob_decompose_app :
Glob_term.glob_constr ->
Glob_term.glob_constr * Glob_term.glob_constr listSource
val glob_make_eq :
?typ:Glob_term.glob_constr ->
Glob_term.glob_constr ->
Glob_term.glob_constr ->
Glob_term.glob_constrSource
val alpha_pat :
Names.Id.Map.key list ->
Glob_term.cases_pattern ->
Glob_term.cases_pattern * Names.Id.Map.key list * Names.Id.t Names.Id.Map.tSource
val replace_var_by_term :
Names.Id.t ->
Glob_term.glob_constr ->
Glob_term.glob_constr ->
Glob_term.glob_constrSource
val eq_cases_pattern :
Environ.env ->
Glob_term.cases_pattern ->
Glob_term.cases_pattern ->
boolSource
val resolve_and_replace_implicits :
EConstr.types ->
Environ.env ->
Evd.evar_map ->
Glob_term.glob_constr ->
Glob_term.glob_constr