package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
type proof = t
  • deprecated please use [Proof.t]
val proof : t -> Goal.goal list * (Goal.goal list * Goal.goal list) list * Goal.goal list * Goal.goal list * Evd.evar_map
type !'a pre_goals = {
  1. fg_goals : 'a list;
  2. bg_goals : ('a list * 'a list) list;
  3. shelved_goals : 'a list;
  4. given_up_goals : 'a list;
}
val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> 'a pre_goals
val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> t
val dependent_start : Proofview.telescope -> t
val initial_goals : t -> (EConstr.constr * EConstr.types) list
val initial_euctx : t -> UState.t
val is_done : t -> bool
val is_complete : t -> bool
val partial_proof : t -> EConstr.constr list
val compact : t -> t
exception UnfinishedProof
exception HasShelvedGoals
exception HasGivenUpGoals
exception HasUnresolvedEvar
val return : t -> Evd.evar_map
type 'a focus_kind
val new_focus_kind : unit -> 'a focus_kind
type 'a focus_condition
val no_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
val focus : 'a focus_condition -> 'a -> int -> t -> t
val focus_id : 'aa focus_condition -> 'a -> Names.Id.t -> t -> t
exception FullyUnfocused
exception CannotUnfocusThisWay
exception NoSuchGoals of int * int
val unfocus : 'a focus_kind -> t -> unit -> t
val unfocused : t -> bool
exception NoSuchFocus
val get_at_focus : 'a focus_kind -> t -> 'a
val is_last_focus : 'a focus_kind -> t -> bool
val no_focused_goal : t -> bool
val run_tactic : Environ.env -> unit Proofview.tactic -> t -> t * (bool * Proofview_monad.Info.tree)
val maximal_unfocus : 'a focus_kind -> t -> t
val in_proof : t -> (Evd.evar_map -> 'a) -> 'a
val unshelve : t -> t
val pr_proof : t -> Pp.t
module V82 : sig ... end
val all_goals : t -> Goal.Set.t