From 2e78edb4b8212cc5ab394fde168fc5241ad01660 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 21 Nov 2018 10:31:07 -0800
Subject: Remove undocumented "Proof using Clear Unused" flag

---
 vernac/vernacentries.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a157e01fc1..629df48c82 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1035,13 +1035,9 @@ let vernac_set_used_variables e =
       user_err ~hdr:"vernac_set_used_variables"
         (str "Unknown variable: " ++ Id.print id))
     l;
-  let _, to_clear = Proof_global.set_used_variables l in
-  let to_clear = List.map (fun x -> x.CAst.v) to_clear in
+  ignore (Proof_global.set_used_variables l);
   Proof_global.with_current_proof begin fun _ p ->
-    if List.is_empty to_clear then (p, ())
-    else
-      let tac = Tactics.clear to_clear in
-      fst (Pfedit.solve Goal_select.SelectAll None tac p), ()
+    (p, ())
   end
 
 (*****************************)
-- 
cgit v1.2.3