package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.1.tar.gz
md5=13d2793fc6413aac5168822313e4864e
sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42
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