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.

Like tclEVARS but also checks whether goals have been solved.

Set the global environment of the 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.

tclSETGOALS gls sets goals gls as the goals being under focus. If a goal is already solved, it is not set.

tclGETGOALS returns the list of goals under focus.

tclGETSHELF returns the list of goals on the shelf.

Sets the evar universe context.

Clears the future goals store in the proof view.

Give the evars the status of a goal (changes their source location and makes them unresolvable for type classes.

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.

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.

undefined sigma l applies advance to the goals of l, then returns the subset of resulting goals which have not yet been defined

update_sigma_univs lifts UState.update_sigma_univs to the proofview