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 : 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.

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 tclSETSHELF : Evar.t list -> unit tactic: tclSETSHELF gls sets goals gls as the current shelf.

val tclGETSHELF : Evar.t list tactic: tclGETSHELF returns the list of goals on the shelf.

val tclPUTSHELF : Evar.t list -> unit tactic: tclPUTSHELF appends goals to the shelf.

val tclPUTGIVENUP : Evar.t list -> unit tactic: tclPUTGIVENUP add an given up goal.

val tclEVARUNIVCONTEXT : UState.t -> unit tactic: Sets the evar universe context.

val reset_future_goals : proofview -> proofview: Clears the future goals store in the proof view.

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