Module `Clenvtac`

Legacy components of the previous proof engine.

val unify : ?⁠flags:Unification.unify_flags -> EConstr.constr -> unit Proofview.tactic: Tactics

val clenv_refine : ?⁠with_evars:bool -> ?⁠with_classes:bool -> Clenv.clausenv -> unit Proofview.tactic
val res_pf : ?⁠with_evars:bool -> ?⁠with_classes:bool -> ?⁠flags:Unification.unify_flags -> Clenv.clausenv -> unit Proofview.tactic
val clenv_pose_dependent_evars : ?⁠with_evars:bool -> Clenv.clausenv -> Clenv.clausenv
val clenv_value_cast_meta : Clenv.clausenv -> EConstr.constr