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.
type clausenv
val clenv_evd : clausenv -> Evd.evar_map
val clenv_meta_list : clausenv -> Unification.Meta.t
val update_clenv_evd : clausenv -> Evd.evar_map -> Unification.Meta.t -> clausenv
val clenv_strip_proj_params : clausenv -> clausenv
val clenv_refresh : Environ.env -> Evd.evar_map -> UnivGen.sort_context_set option -> clausenv -> clausenv
val clenv_arguments : clausenv -> Constr.metavariable list
val clenv_value : clausenv -> EConstr.constr

subject of clenv (instantiated)

val clenv_type : clausenv -> EConstr.types

type of clenv (instantiated)

val mk_clenv_from_n : Environ.env -> Evd.evar_map -> int -> (EConstr.constr * EConstr.types) -> clausenv
linking of clenvs
Bindings
val clenv_independent : clausenv -> Constr.metavariable list

bindings 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 -> Names.Name.t list * int

start with a clenv to refine with a given term with bindings

val make_clenv_binding_apply : Environ.env -> Evd.evar_map -> int option -> (EConstr.constr * EConstr.constr) -> EConstr.constr Tactypes.bindings -> clausenv

the 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 clenv_push_prod : clausenv -> (Constr.metavariable * bool * clausenv) option

if the clause is a product, add an extra meta for this product

Clenv tactics
val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:Unification.unify_flags -> clausenv -> unit Proofview.tactic
val case_pf : ?with_evars:bool -> dep:bool -> (EConstr.constr * EConstr.types) -> unit Proofview.tactic
val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv
val pr_clenv : clausenv -> Pp.t

Pretty-print (debug only)

module Internal : sig ... end