Remove undocumented "Proof using Clear Unused" flag

1 files changed, 2 insertions, 6 deletions

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
 
 (*****************************)