package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
val proof : t -> Goal.goal list * (Goal.goal list * Goal.goal list) list * Goal.goal list * Goal.goal list * Evd.evar_map
  • deprecated use [Proof.data]
val initial_goals : t -> (EConstr.constr * EConstr.types) list
  • deprecated use [Proof.data]
val initial_euctx : t -> UState.t
  • deprecated use [Proof.data]
type data = {
  1. sigma : Evd.evar_map;
  2. goals : Evar.t list;
  3. entry : Proofview.entry;
  4. stack : (Evar.t list * Evar.t list) list;
  5. shelf : Evar.t list;
  6. given_up : Evar.t list;
  7. initial_euctx : UState.t;
  8. name : Names.Id.t;
  9. poly : bool;
}
val data : t -> data
type !'a pre_goals = {
  1. fg_goals : 'a list;
    (*
    • deprecated use [Proof.data]
    *)
  2. bg_goals : ('a list * 'a list) list;
    (*
    • deprecated use [Proof.data]
    *)
  3. shelved_goals : 'a list;
    (*
    • deprecated use [Proof.data]
    *)
  4. given_up_goals : 'a list;
    (*
    • deprecated use [Proof.data]
    *)
}
  • deprecated use [Proof.data]
val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> 'a pre_goals
  • deprecated use [Proof.data]
val start : name:Names.Id.t -> poly:bool -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t
val dependent_start : name:Names.Id.t -> poly:bool -> Proofview.telescope -> t
val is_done : t -> bool
val is_complete : t -> bool
val partial_proof : t -> EConstr.constr list
val compact : t -> t
type open_error_reason =
  1. | UnfinishedProof
  2. | HasGivenUpGoals
exception OpenProof of Names.Id.t option * open_error_reason
val return : ?pid:Names.Id.t -> 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