package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module ProofSource

Sourcetype t
Sourcetype 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

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

update_sigma_univs lifts UState.update_sigma_univs to the proof

Sourcetype open_error_reason =
  1. | UnfinishedProof
  2. | HasGivenUpGoals
Sourceexception OpenProof of Names.Id.t option * open_error_reason
Sourceval return : ?pid:Names.Id.t -> ?allow_given_up:bool -> t -> Evd.evar_map
Sourcetype 'a focus_kind
Sourceval new_focus_kind : unit -> 'a focus_kind
Sourcetype 'a focus_condition
Sourceval no_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
Sourceval done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
Sourceval focus : 'a focus_condition -> 'a -> int -> t -> t
Sourceval focus_id : 'a focus_condition -> 'a -> Names.Id.t -> t -> t
Sourceexception FullyUnfocused
Sourceexception CannotUnfocusThisWay
Sourceexception NoSuchGoals of int * int
Sourceexception NoSuchGoal of Names.Id.t option
Sourceval unfocus : 'a focus_kind -> t -> unit -> t
Sourceval unfocused : t -> bool
Sourceexception NoSuchFocus
Sourceval get_at_focus : 'a focus_kind -> t -> 'a
Sourceval is_last_focus : 'a focus_kind -> t -> bool
Sourceval no_focused_goal : t -> bool
Sourceval run_tactic : Environ.env -> 'a Proofview.tactic -> t -> t * (bool * Proofview_monad.Info.tree) * 'a
Sourceval maximal_unfocus : 'a focus_kind -> t -> t
Sourceval unshelve : t -> t
Sourceval goal_uid : Evar.t -> string
Sourceval pr_proof : t -> Pp.t
Sourceval background_subgoals : t -> Evar.t list
Sourceval all_goals : t -> Evar.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.

Sourceval solve : ?with_end_tac:unit Proofview.tactic -> Goal_select.t -> int option -> unit Proofview.tactic -> t -> t * bool
Sourceval use_unification_heuristics : unit -> bool

Option telling if unification heuristics should be used.

Sourceval 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.

Sourceexception SuggestNoSuchGoals of int * t
Sourceval get_goal_context_gen : t -> int -> Evd.evar_map * Environ.env

Helpers to obtain proof state when in an interactive proof

Sourceval 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