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 currentevar_map
bysigma
. Ifsigma
has new unresolvedevar
-s they will not appear as goal. If goals have been solved insigma
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 goalsgls
to the ones currently being proved, appending them to the list of focused goals. If a goal is already solved, it is not added.
val tclNEWSHELVED : Evar.t list -> unit tactic
tclNEWSHELVED gls
adds the goalsgls
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 goalsgls
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
returnsSome g'
ifg'
is undefined and is the current avatar ofg
(for instanceg
was changed byclear
intog'
). It returnsNone
ifg
has been (partially) solved.
val undefined : Evd.evar_map -> Proofview_monad.goal_with_state list -> Proofview_monad.goal_with_state list
undefined sigma l
appliesadvance
to the goals ofl
, then returns the subset of resulting goals which have not yet been defined