From e4aa9817115b3d27eb7fca8fed86ffe397b868ad Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Fri, 12 Sep 2014 16:58:37 +0200
Subject: While we don't have a clean alternative to Clenvtac, add a primitive
 for tclEVARS which might solve existing goals.

---
 proofs/proofview.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'proofs/proofview.ml')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index bc6ce4fc6..a97add1ce 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -804,6 +804,9 @@ module V82 = struct
   let tclEVARS evd =
     Proof.modify (fun ps -> { ps with solution = evd })
 
+  let tclEVARSADVANCE evd =
+    Proof.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb })
+
   let tclEVARUNIVCONTEXT ctx = 
     Proof.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
       
-- 
cgit v1.2.3