From 65e0522033ea47ed479227be30a92fceaa8c6358 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Mar 2016 02:20:10 +0100
Subject: Replacing the interpretation of Proof using ... with a proper code.

---
 toplevel/vernacentries.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 02f8c17175..fd125b335c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -884,13 +884,13 @@ let vernac_set_used_variables e =
         (str "Unknown variable: " ++ pr_id id))
     l;
   let _, to_clear = set_used_variables l in
-  (** FIXME: too fragile *)
-  let open Tacexpr in
-  let tac = { mltac_plugin = "coretactics"; mltac_tactic = "clear" } in
-  let tac = { mltac_name = tac; mltac_index = 0 } in
-  let arg = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Constrarg.wit_var)) to_clear in
-  let tac = if List.is_empty to_clear then TacId [] else TacML (Loc.ghost, tac, [TacGeneric arg]) in
-  vernac_solve SelectAll None tac false
+  let to_clear = List.map snd to_clear in
+  Proof_global.with_current_proof begin fun _ p ->
+    if List.is_empty to_clear then (p, ())
+    else
+      let tac = Proofview.V82.tactic (Tactics.clear to_clear) in
+      fst (solve SelectAll None tac p), ()
+  end
 
 
 (*****************************)
-- 
cgit v1.2.3