# Module `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.

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

`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 mark_as_unresolvables : proofview -> Evar.t list -> proofview`

`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