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

(limited to 'toplevel')

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


From ce2ffd090bd64963279cbbb84012d1b266ed9918 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Mar 2016 01:43:29 +0100
Subject: Moving VernacSolve to an EXTEND-based definition.

---
 toplevel/vernacentries.ml  | 31 -------------------------------
 toplevel/vernacentries.mli |  2 ++
 2 files changed, 2 insertions(+), 31 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fd125b335c..8ba5eb3f7d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -826,35 +826,6 @@ let vernac_declare_class id =
 let command_focus = Proof.new_focus_kind ()
 let focus_command_cond = Proof.no_cond command_focus
 
-
-let print_info_trace = ref None
-
-let _ = let open Goptions in declare_int_option {
-  optsync = true;
-  optdepr = false;
-  optname = "print info trace";
-  optkey = ["Info" ; "Level"];
-  optread = (fun () -> !print_info_trace);
-  optwrite = fun n -> print_info_trace := n;
-}
-
-let vernac_solve n info tcom b =
-  if not (refining ()) then
-    error "Unknown command of the non proof-editing mode.";
-  let status = Proof_global.with_current_proof (fun etac p ->
-    let with_end_tac = if b then Some etac else None in
-    let global = match n with SelectAll -> true | _ -> false in
-    let info = Option.append info !print_info_trace in
-    let (p,status) =
-      solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
-    in
-    (* in case a strict subtree was completed,
-       go back to the top of the prooftree *)
-    let p = Proof.maximal_unfocus command_focus p in
-    p,status) in
-    if not status then Pp.feedback Feedback.AddedAxiom
- 
-
   (* A command which should be a tactic. It has been
      added by Christine to patch an error in the design of the proof
      machine, and enables to instantiate existential variables when
@@ -892,7 +863,6 @@ let vernac_set_used_variables e =
       fst (solve SelectAll None tac p), ()
   end
 
-
 (*****************************)
 (* Auxiliary file management *)
 
@@ -1909,7 +1879,6 @@ let interp ?proof ~loc locality poly c =
   | VernacDeclareClass id -> vernac_declare_class id
 
   (* Solving *)
-  | VernacSolve (n,info,tac,b) -> vernac_solve n info tac b
   | VernacSolveExistential (n,c) -> vernac_solve_existential n c
 
   (* Auxiliary file and library management *)
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 451ccdb4d4..4a59b1299b 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -59,3 +59,5 @@ val vernac_end_proof :
   ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
 
 val with_fail : bool -> (unit -> unit) -> unit
+
+val command_focus : unit Proof.focus_kind
-- 
cgit v1.2.3