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;
    (*

    A representation of the evar_map EJGA wouldn't it better to just return the proofview?

    *)
  2. goals : Evar.t list;
    (*

    Focused goals

    *)
  3. entry : Proofview.entry;
    (*

    Entry for the proofview

    *)
  4. stack : (Evar.t list * Evar.t list) list;
    (*

    A representation of the focus stack

    *)
  5. name : Names.Id.t;
    (*

    The name of the theorem whose proof is being constructed

    *)
  6. poly : bool;
    (*

    polymorphism

    *)
}
val data : t -> data
val start : name:Names.Id.t -> poly:bool -> ?typing_flags:Declarations.typing_flags -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t
val dependent_start : name:Names.Id.t -> poly:bool -> ?typing_flags:Declarations.typing_flags -> Proofview.telescope -> t
val is_done : t -> bool
val is_complete : t -> bool
val partial_proof : t -> EConstr.constr list
val compact : t -> t
val update_sigma_univs : UGraph.t -> t -> t

update_sigma_univs lifts UState.update_sigma_univs to the proof

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

solve (SelectNth n) tac applies tactic tac to the nth subgoal of the current focused proof. solve SelectAll tac applies tac to all subgoals.

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

Option telling if unification heuristics should be used.

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

A variant of the above function that handles open terms as well. Caveat: all effects are purged in the returned term at the end, but other evars solved by side-effects are NOT purged, so that unexpected failures may occur. Ideally all code using this function should be rewritten in the monad.

exception SuggestNoSuchGoals of int * t
val get_goal_context_gen : t -> int -> Evd.evar_map * Environ.env

Helpers to obtain proof state when in an interactive proof

val get_proof_context : t -> Evd.evar_map * Environ.env

get_proof_context () gets the goal context for the first subgoal of the proof

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