diff options
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 635f2fd47a..adb6ec37d4 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -275,6 +275,10 @@ module V82 : sig type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val tactic : tac -> unit tactic + (* normalises the evars in the goals, and stores the result in + solution. *) + val nf_evar_goals : unit tactic + val tclEVARS : Evd.evar_map -> unit tactic val has_unresolved_evar : proofview -> bool |