package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (5)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.proofs/Proof/index.html

Module ProofSource

Sourcetype t
Sourcetype data = private {
  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 : PolyFlags.t;
    (*

    Universe polymorphism

    *)
}
Sourceval data : t -> data
Sourceval start : name:Names.Id.t -> poly:PolyFlags.t -> ?typing_flags:Declarations.typing_flags -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t
Sourceval dependent_start : name:Names.Id.t -> poly:PolyFlags.t -> ?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 'a focus_kind
Sourceval new_focus_kind : string -> '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 -> Libnames.qualid -> t -> t
Sourceexception FullyUnfocused
Sourceexception CannotUnfocusThisWay
Sourceexception NoSuchGoals of int * int
Sourceexception NoSuchGoal of Libnames.qualid option
Sourceval unfocus : 'a focus_kind -> t -> unit -> t
Sourceval unfocused : t -> bool
Sourceval unfocus_all : t -> t

Unfocus everything (fail if no allowed).

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 * (Environ.env * 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 (select_nth 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 -> Environ.env -> 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.

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

Sourceval purge_side_effects : t -> t * Evd.side_effects