package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val subgoals : t -> Goal.goal list Evd.sigma
  • deprecated Use the first and fifth argument of [Proof.proof]
val background_subgoals : t -> Goal.goal list Evd.sigma
val top_goal : t -> Goal.goal Evd.sigma
val top_evars : t -> Evar.t list
val grab_evars : t -> t
val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t