package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
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