package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
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. name : Names.Id.t;
  8. poly : bool;
}
val data : t -> 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
exception NoSuchGoal of Names.Id.t option
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 -> 'a Proofview.tactic -> t -> t * (bool * Proofview_monad.Info.tree) * 'a
val maximal_unfocus : 'a focus_kind -> t -> t
val unshelve : t -> t
val pr_proof : t -> Pp.t
module V82 : sig ... end
val all_goals : t -> Goal.Set.t
val solve : ?with_end_tac:unit Proofview.tactic -> Goal_select.t -> int option -> unit Proofview.tactic -> t -> t * bool
val use_unification_heuristics : unit -> bool
val refine_by_tactic : name:Names.Id.t -> poly:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic -> Constr.constr * Evd.evar_map
exception SuggestNoSuchGoals of int * t
val get_goal_context_gen : t -> int -> Evd.evar_map * Environ.env
val get_proof_context : t -> Evd.evar_map * Environ.env
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