package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
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