Replacing the interpretation of Proof using ... with a proper code.

1 files changed, 7 insertions, 7 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 02f8c1717..fd125b335 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
 
 
 (*****************************)