While we don't have a clean alternative to Clenvtac, add a primitive

for tclEVARS which might solve existing goals.

1 files changed, 5 insertions, 1 deletions

diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 3b2dd7ccd5..94969f3a5c 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -334,8 +334,12 @@ module V82 : sig
   (* normalises the evars in the goals, and stores the result in
      solution. *)
   val nf_evar_goals : unit tactic
-
+    
+  (* Assumes the new evar_map does not change existing goals *)
   val tclEVARS : Evd.evar_map -> unit tactic
+    
+  (* Assumes the new evar_map might be solving some existing goals *)
+  val tclEVARSADVANCE : Evd.evar_map -> unit tactic
 
   (* Set the evar universe context *)
   val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic