package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
val start : info:Info.t -> cinfo:EConstr.t CInfo.t -> Evd.evar_map -> t
val start_derive : f:Names.Id.t -> name:Names.Id.t -> info:Info.t -> Proofview.telescope -> t
val start_equations : name:Names.Id.t -> info:Info.t -> hook:(pm:OblState.t -> Names.Constant.t list -> Evd.evar_map -> OblState.t) -> types: (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list -> Evd.evar_map -> Proofview.telescope -> t
val start_with_initialization : info:Info.t -> cinfo:Constr.t CInfo.t -> Evd.evar_map -> t
type mutual_info = bool * lemma_possible_guards * Constr.t option list option
val start_mutual_with_initialization : info:Info.t -> cinfo:Constr.t CInfo.t list -> mutual_info:mutual_info -> Evd.evar_map -> int list option -> t
val save : pm:OblState.t -> proof:t -> opaque:Vernacexpr.opacity_flag -> idopt:Names.lident option -> OblState.t * Names.GlobRef.t list
val save_regular : proof:t -> opaque:Vernacexpr.opacity_flag -> idopt:Names.lident option -> Names.GlobRef.t list
val save_admitted : pm:OblState.t -> proof:t -> OblState.t
val by : unit Proofview.tactic -> t -> t * bool
val get : t -> Proof.t
val get_name : t -> Names.Id.t
val fold : f:(Proof.t -> 'a) -> t -> 'a
val map : f:(Proof.t -> Proof.t) -> t -> t
val map_fold : f:(Proof.t -> Proof.t * 'a) -> t -> t * 'a
val map_fold_endline : f:(unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
val set_used_variables : t -> Names.Id.t list -> Constr.named_context * t
val get_used_variables : t -> Names.Id.Set.t option
val compact : t -> t
val update_sigma_univs : UGraph.t -> t -> t
val get_open_goals : t -> int
val get_goal_context : t -> int -> Evd.evar_map * Environ.env
val get_current_goal_context : t -> Evd.evar_map * Environ.env
val get_current_context : t -> Evd.evar_map * Environ.env
type closed_proof_output
val return_proof : t -> closed_proof_output
val return_partial_proof : t -> closed_proof_output
type proof_object
val close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> t -> proof_object
val close_future_proof : feedback_id:Stateid.t -> t -> closed_proof_output Future.computation -> proof_object
val save_lemma_admitted_delayed : pm:OblState.t -> proof:proof_object -> OblState.t
val save_lemma_proved_delayed : pm:OblState.t -> proof:proof_object -> idopt:Names.lident option -> OblState.t * Names.GlobRef.t list
val get_po_name : proof_object -> Names.Id.t