Module Clenv
This file defines clausenv, which is a deprecated way to handle open terms in the proof engine. This API is legacy.
The Type of Constructions clausale environments.
val clenv_evd : clausenv -> Evd.evar_mapval update_clenv_evd : clausenv -> Evd.evar_map -> clausenvval clenv_strip_proj_params : clausenv -> clausenvval clenv_refresh : Environ.env -> Evd.evar_map -> UnivGen.sort_context_set option -> clausenv -> clausenvval clenv_arguments : clausenv -> Constr.metavariable listval clenv_value : clausenv -> EConstr.constrsubject of clenv (instantiated)
val clenv_type : clausenv -> EConstr.typestype of clenv (instantiated)
val mk_clenv_from : Environ.env -> Evd.evar_map -> (EConstr.constr * EConstr.types) -> clausenvval mk_clenv_from_n : Environ.env -> Evd.evar_map -> int -> (EConstr.constr * EConstr.types) -> clausenv
linking of clenvs
val clenv_instantiate : ?flags:Unification.unify_flags -> ?submetas:(Constr.metavariable * Evd.clbinding) list -> Constr.metavariable -> clausenv -> (EConstr.constr * EConstr.types) -> clausenv
Bindings
val clenv_independent : clausenv -> Constr.metavariable listbindings where the key is the position in the template of the clenv (dependent or not). Positions can be negative meaning to start from the rightmost argument of the template.
val clenv_missing : clausenv -> Constr.metavariable list
val make_clenv_binding_apply : Environ.env -> Evd.evar_map -> int option -> (EConstr.constr * EConstr.constr) -> EConstr.constr Tactypes.bindings -> clausenvthe arity of the lemma is fixed the optional int tells how many prods of the lemma have to be used use all of them if None
val make_clenv_binding : Environ.env -> Evd.evar_map -> (EConstr.constr * EConstr.constr) -> EConstr.constr Tactypes.bindings -> clausenvval clenv_push_prod : clausenv -> (Constr.metavariable * bool * clausenv) optionif the clause is a product, add an extra meta for this product
Clenv tactics
val unify : ?flags:Unification.unify_flags -> cv_pb:Conversion.conv_pb -> EConstr.constr -> unit Proofview.tacticval res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:Unification.unify_flags -> clausenv -> unit Proofview.tacticval case_pf : ?with_evars:bool -> dep:bool -> (EConstr.constr * EConstr.types) -> unit Proofview.tacticval clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenvval pr_clenv : clausenv -> Pp.tPretty-print (debug only)
module Internal : sig ... end