`Proofview.Unsafe`

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.

`val 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.

`val tclEVARSADVANCE : Evd.evar_map -> unit tactic`

Like `tclEVARS`

but also checks whether goals have been solved.

`val tclSETENV : Environ.env -> unit tactic`

Set the global environment of the tactic

`val 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.

`tclNEWSHELVED gls`

adds the goals `gls`

to the shelf. If a goal is already solved, it is not added.

`val 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.

`val tclGETGOALS : Proofview_monad.goal_with_state list tactic`

`tclGETGOALS`

returns the list of goals under focus.

`val 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.

`val 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.

`val 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.

`val undefined : Evd.evar_map -> Proofview_monad.goal_with_state list -> Proofview_monad.goal_with_state list`

`undefined sigma l`

applies `advance`

to the goals of `l`

, then returns the subset of resulting goals which have not yet been defined