Module Clenv

This file defines clausenv, which is a deprecated way to handle open terms in the proof engine. Most of the API here is legacy except for the evar-based clauses.

The Type of Constructions clausale environments.
type clausenv = {
env : Environ.env;

the typing context

evd : Evd.evar_map;

the mapping from metavar and evar numbers to their types and values

templval : EConstr.constr Evd.freelisted;

the template which we are trying to fill out

templtyp : EConstr.constr Evd.freelisted;

its type

}
val clenv_value : clausenv -> EConstr.constr

subject of clenv (instantiated)

val clenv_type : clausenv -> EConstr.types

type of clenv (instantiated)

val clenv_meta_type : clausenv -> Constr.metavariable -> EConstr.types

type of a meta in clenv context

val mk_clenv_from : Proofview.Goal.t -> (EConstr.constr * EConstr.types) -> clausenv
val mk_clenv_from_n : Proofview.Goal.t -> int option -> (EConstr.constr * EConstr.types) -> clausenv
val mk_clenv_from_env : Environ.env -> Evd.evar_map -> int option -> (EConstr.constr * EConstr.types) -> clausenv
linking of clenvs
val clenv_fchain : ?⁠with_univs:bool -> ?⁠flags:Unification.unify_flags -> Constr.metavariable -> clausenv -> clausenv -> clausenv
Unification with clenvs
val clenv_unify : ?⁠flags:Unification.unify_flags -> Evd.conv_pb -> EConstr.constr -> EConstr.constr -> clausenv -> clausenv

Unifies two terms in a clenv. The boolean is allow_K (see Unification)

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 -> Constr.metavariable list
exception NoSuchBinding

for the purpose of inversion tactics

val clenv_constrain_last_binding : EConstr.constr -> clausenv -> clausenv
val clenv_unify_meta_types : ?⁠flags:Unification.unify_flags -> clausenv -> clausenv
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 make_clenv_binding : Environ.env -> Evd.evar_map -> (EConstr.constr * EConstr.constr) -> EConstr.constr Tactypes.bindings -> clausenv
exception NotExtensibleClause

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

val clenv_push_prod : clausenv -> clausenv
Clenv tactics
val unify : ?⁠flags:Unification.unify_flags -> EConstr.constr -> unit Proofview.tactic
val res_pf : ?⁠with_evars:bool -> ?⁠with_classes:bool -> ?⁠flags:Unification.unify_flags -> clausenv -> unit Proofview.tactic
val clenv_pose_dependent_evars : ?⁠with_evars:bool -> clausenv -> clausenv
val pr_clenv : clausenv -> Pp.t
Pretty-print (debug only)
Evar-based clauses
type hole = {
hole_evar : EConstr.constr;

The hole itself. Guaranteed to be an evar.

hole_type : EConstr.types;

Type of the hole in the current environment.

hole_deps : bool;

Whether the remainder of the clause was dependent in the hole. Note that because let binders are substituted, it does not mean that it actually appears somewhere in the returned clause.

hole_name : Names.Name.t;

Name of the hole coming from its binder.

}
type clause = {
cl_holes : hole list;
cl_concl : EConstr.types;
}
val make_evar_clause : Environ.env -> Evd.evar_map -> ?⁠len:int -> EConstr.types -> Evd.evar_map * clause

An evar version of make_clenv_binding. Given a type t, evar_environments env sigma ~len t bl tries to eliminate at most len products of the type t by filling it with evars. It returns the resulting type together with the list of holes generated. Assumes that t is well-typed in the environment.

val solve_evar_clause : Environ.env -> Evd.evar_map -> bool -> clause -> EConstr.constr Tactypes.bindings -> Evd.evar_map

solve_evar_clause env sigma hyps cl bl tries to solve the holes contained in cl according to the bl argument. Assumes that bl are well-typed in the environment. The boolean hyps is a compatibility flag that allows to consider arguments to be dependent only when they appear in hypotheses and not in the conclusion. This boolean is only used when bl is of the form ImplicitBindings _.