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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct