package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
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 resolve_and_replace_implicits :
?flags:Pretyping.inference_flags ->
?expected_type:Pretyping.typing_constraint ->
Environ.env ->
Evd.evar_map ->
Glob_term.glob_constr ->
Glob_term.glob_constr