package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824
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