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 : Proofview_monad.goal_with_state list -> unit tactic
tclNEWGOALS gls
adds the goals gls
to the ones currently being proved, appending them to the list of focused goals. 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