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 (3)

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.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.engine/Proofview/Unsafe/index.html

Module Proofview.UnsafeSource

The primitives in the Unsafe module should be avoided as much as possible, since they can make the proof state inconsistent. They are nevertheless helpful, in particular when interfacing the pretyping and the proof engine.

Sourceval tclEVARS : Evd.evar_map -> unit tactic

tclEVARS sigma replaces the current evar_map by sigma. If sigma has new unresolved evar-s they will not appear as goal. If goals have been solved in sigma they will still appear as unsolved goals.

Sourceval tclEVARSADVANCE : Evd.evar_map -> unit tactic

Like tclEVARS but also checks whether goals have been solved.

Sourceval tclSETENV : Environ.env -> unit tactic

Set the global environment of the tactic

Sourceval tclNEWGOALS : ?before:bool -> Proofview_monad.goal_with_state list -> unit tactic

tclNEWGOALS ~before gls adds the goals gls to the ones currently being proved. If before is true, it prepends them to the list of focused goals, otherwise it appends them (default). If a goal is already solved, it is not added.

Sourceval tclNEWSHELVED : Evar.t list -> unit tactic

tclNEWSHELVED gls adds the goals gls to the shelf. If a goal is already solved, it is not added.

Sourceval tclSETGOALS : Proofview_monad.goal_with_state list -> unit tactic

tclSETGOALS gls sets goals gls as the goals being under focus. If a goal is already solved, it is not set.

tclGETGOALS returns the list of goals under focus.

Sourceval tclGETSHELF : Evar.t list tactic

tclGETSHELF returns the list of goals on the shelf.

Sourceval tclEVARUNIVCONTEXT : UState.t -> unit tactic

Sets the evar universe context.

Sourceval push_future_goals : proofview -> proofview

Clears the future goals store in the proof view.

Sourceval mark_as_goals : Evd.evar_map -> Evar.t list -> Evd.evar_map

Give the evars the status of a goal (changes their source location and makes them unresolvable for type classes.

Sourceval mark_unresolvables : Evd.evar_map -> Evar.t list -> Evd.evar_map

Make some evars unresolvable for type classes. We need two functions as some functions use the proofview and others directly manipulate the undelying evar_map.

Sourceval mark_as_unresolvables : proofview -> Evar.t list -> proofview
Sourceval advance : Evd.evar_map -> Evar.t -> Evar.t option

advance sigma g returns Some g' if g' is undefined and is the current avatar of g (for instance g was changed by clear into g'). It returns None if g has been (partially) solved.

undefined sigma l applies advance to the goals of l, then returns the subset of resulting goals which have not yet been defined

Sourceval update_sigma_univs : UGraph.t -> proofview -> proofview

update_sigma_univs lifts UState.update_sigma_univs to the proofview