diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 8 |
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 (*****************************) |