package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type proof
val proof : proof -> 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 : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> 'a pre_goals
val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof
val dependent_start : Proofview.telescope -> proof
val initial_goals : proof -> (EConstr.constr * EConstr.types) list
val initial_euctx : proof -> Evd.evar_universe_context
val is_done : proof -> bool
val is_complete : proof -> bool
val partial_proof : proof -> EConstr.constr list
val compact : proof -> proof
exception UnfinishedProof
exception HasShelvedGoals
exception HasGivenUpGoals
exception HasUnresolvedEvar
val return : proof -> 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 -> proof -> proof
exception FullyUnfocused
exception CannotUnfocusThisWay
exception NoSuchGoals of int * int
val unfocus : 'a focus_kind -> proof -> unit -> proof
val unfocused : proof -> bool
exception NoSuchFocus
val get_at_focus : 'a focus_kind -> proof -> 'a
val is_last_focus : 'a focus_kind -> proof -> bool
val no_focused_goal : proof -> bool
val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof * (bool * Proofview_monad.Info.tree)
val maximal_unfocus : 'a focus_kind -> proof -> proof
val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a
val unshelve : proof -> proof
val pr_proof : proof -> Pp.std_ppcmds
module V82 : sig ... end
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