Removing tactic compatibility layer from Eqdecide.

1 files changed, 48 insertions, 47 deletions

diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 0effc3136..23c4c0b2d 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -21,11 +21,11 @@ open Namegen
 open Term
 open Declarations
 open Tactics
-open Tacticals
+open Tacticals.New
 open Auto
 open ConstrMatching
 open Hipattern
-open Tacmach
+open Tacmach.New
 open Coqlib
 
 (* This file containts the implementation of the tactics ``Decide
@@ -50,6 +50,7 @@ open Coqlib
    Eduardo Gimenez (30/3/98).
 *)
 
+let clear ids = Proofview.V82.tactic (clear ids)
 let clear_last = (onLastHyp (fun c -> (clear [destVar c])))
 
 let choose_eq eqonleft =
@@ -64,22 +65,22 @@ let choose_noteq eqonleft =
     left_with_bindings false Misctypes.NoBindings
 
 let mkBranches c1 c2 =
-  Tacticals.New.tclTHENLIST
+  tclTHENLIST
     [Proofview.V82.tactic (generalize [c2]);
      Simple.elim c1;
      intros;
-     Tacticals.New.onLastHyp Simple.case;
-     Proofview.V82.tactic clear_last;
+     onLastHyp Simple.case;
+     clear_last;
      intros]
 
 let solveNoteqBranch side =
-  Tacticals.New.tclTHEN (choose_noteq side)
-    (Tacticals.New.tclTHEN introf
-      (Tacticals.New.onLastHypId (fun id -> Extratactics.discrHyp id)))
+  tclTHEN (choose_noteq side)
+    (tclTHEN introf
+      (onLastHypId (fun id -> Extratactics.discrHyp id)))
 
 (* Constructs the type {c1=c2}+{~c1=c2} *)
 
-let mkDecideEqGoal eqonleft op rectype c1 c2 g =
+let mkDecideEqGoal eqonleft op rectype c1 c2 =
   let equality    = mkApp(build_coq_eq(), [|rectype; c1; c2|]) in
   let disequality = mkApp(build_coq_not (), [|equality|]) in
   if eqonleft then mkApp(op, [|equality; disequality |])
@@ -88,30 +89,33 @@ let mkDecideEqGoal eqonleft op rectype c1 c2 g =
 
 (* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *)
 
+let idx = Id.of_string "x"
+let idy = Id.of_string "y"
+
 let mkGenDecideEqGoal rectype g =
   let hypnames = pf_ids_of_hyps g in
-  let xname    = next_ident_away (Id.of_string "x") hypnames
-  and yname    = next_ident_away (Id.of_string "y") hypnames in
+  let xname    = next_ident_away idx hypnames
+  and yname    = next_ident_away idy hypnames in
   (mkNamedProd xname rectype
      (mkNamedProd yname rectype
         (mkDecideEqGoal true (build_coq_sumbool ())
-          rectype (mkVar xname) (mkVar yname) g)))
+          rectype (mkVar xname) (mkVar yname))))
 
 let eqCase tac =
-  (Tacticals.New.tclTHEN intro
-  (Tacticals.New.tclTHEN (Tacticals.New.onLastHyp Equality.rewriteLR)
-  (Tacticals.New.tclTHEN (Proofview.V82.tactic clear_last)
+  (tclTHEN intro
+  (tclTHEN (onLastHyp Equality.rewriteLR)
+  (tclTHEN clear_last
   tac)))
 
 let diseqCase eqonleft =
   let diseq  = Id.of_string "diseq" in
   let absurd = Id.of_string "absurd" in
-  (Tacticals.New.tclTHEN (intro_using diseq)
-  (Tacticals.New.tclTHEN (choose_noteq eqonleft)
-  (Tacticals.New.tclTHEN  (Proofview.V82.tactic red_in_concl)
-  (Tacticals.New.tclTHEN  (intro_using absurd)
-  (Tacticals.New.tclTHEN  (Proofview.V82.tactic (Simple.apply (mkVar diseq)))
-  (Tacticals.New.tclTHEN  (Extratactics.injHyp absurd)
+  (tclTHEN (intro_using diseq)
+  (tclTHEN (choose_noteq eqonleft)
+  (tclTHEN  (Proofview.V82.tactic red_in_concl)
+  (tclTHEN  (intro_using absurd)
+  (tclTHEN  (Proofview.V82.tactic (Simple.apply (mkVar diseq)))
+  (tclTHEN  (Extratactics.injHyp absurd)
             (full_trivial [])))))))
 
 open Proofview.Notations
@@ -125,22 +129,20 @@ let match_eqdec c =
 (* /spiwack *)
 
 let solveArg eqonleft op a1 a2 tac =
-  Proofview.Goal.enter begin fun gl ->
-  let rectype = Tacmach.New.of_old (fun g -> pf_type_of g a1) gl in
-  let decide =
-    Tacmach.New.of_old (fun g -> mkDecideEqGoal eqonleft op rectype a1 a2 g) gl
-  in
+  Proofview.Goal.raw_enter begin fun gl ->
+  let rectype = pf_type_of gl a1 in
+  let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in
   let subtacs =
     if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto]
     else [diseqCase eqonleft;eqCase tac;default_auto] in
-  (Tacticals.New.tclTHENS (Proofview.V82.tactic (elim_type decide)) subtacs)
+  (tclTHENS (Proofview.V82.tactic (elim_type decide)) subtacs)
   end
 
 let solveEqBranch rectype =
   Proofview.tclORELSE
     begin
-      Proofview.Goal.enter begin fun gl ->
-        let concl = Proofview.Goal.concl gl in
+      Proofview.Goal.raw_enter begin fun gl ->
+        let concl = pf_nf_concl gl in
         match_eqdec concl >>= fun (eqonleft,op,lhs,rhs,_) ->
           let (mib,mip) = Global.lookup_inductive rectype in
           let nparams   = mib.mind_nparams in
@@ -149,7 +151,7 @@ let solveEqBranch rectype =
           and largs   = getargs lhs in
           List.fold_right2
             (solveArg eqonleft op) largs rargs
-            (Tacticals.New.tclTHEN (choose_eq eqonleft) intros_reflexivity)
+            (tclTHEN (choose_eq eqonleft) intros_reflexivity)
       end
     end
     begin function
@@ -166,17 +168,17 @@ let hd_app c = match kind_of_term c with
 let decideGralEquality =
   Proofview.tclORELSE
     begin
-      Proofview.Goal.enter begin fun gl ->
-        let concl = Proofview.Goal.concl gl in
+      Proofview.Goal.raw_enter begin fun gl ->
+        let concl = pf_nf_concl gl in
         match_eqdec concl >>= fun (eqonleft,_,c1,c2,typ) ->
-        let headtyp = Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) gl in
+        let headtyp = hd_app (pf_compute gl typ) in
         begin match kind_of_term headtyp with
         | Ind mi -> Proofview.tclUNIT mi
-        | _ -> Proofview.tclZERO (UserError ("",Pp.str"This decision procedure only works for inductive objects."))
+        | _ -> tclZEROMSG (Pp.str"This decision procedure only works for inductive objects.")
         end >>= fun rectype ->
-          (Tacticals.New.tclTHEN
+          (tclTHEN
              (mkBranches c1 c2)
-             (Tacticals.New.tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
+             (tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
       end
     end
     begin function
@@ -185,24 +187,23 @@ let decideGralEquality =
       | e -> Proofview.tclZERO e
     end
 
-let decideEqualityGoal = Tacticals.New.tclTHEN intros decideGralEquality
+let decideEqualityGoal = tclTHEN intros decideGralEquality
 
 let decideEquality rectype =
-  Proofview.Goal.enter begin fun gl ->
-  let decide = Tacmach.New.of_old (mkGenDecideEqGoal rectype) gl in
-  (Tacticals.New.tclTHENS (cut decide) [default_auto;decideEqualityGoal])
+  Proofview.Goal.raw_enter begin fun gl ->
+  let decide = mkGenDecideEqGoal rectype gl in
+  (tclTHENS (cut decide) [default_auto;decideEqualityGoal])
   end
 
 
 (* The tactic Compare *)
 
 let compare c1 c2 =
-  Proofview.Goal.enter begin fun gl ->
-  let rectype = Tacmach.New.of_old (fun g -> pf_type_of g c1) gl in
-  let decide = Tacmach.New.of_old (fun g -> mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 g) gl in
-  (Tacticals.New.tclTHENS (cut decide)
-            [(Tacticals.New.tclTHEN  intro
-             (Tacticals.New.tclTHEN (Tacticals.New.onLastHyp simplest_case)
-                       (Proofview.V82.tactic clear_last)));
+  Proofview.Goal.raw_enter begin fun gl ->
+  let rectype = pf_type_of gl c1 in
+  let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in
+  (tclTHENS (cut decide)
+            [(tclTHEN  intro
+             (tclTHEN (onLastHyp simplest_case) clear_last));
              decideEquality rectype])
   end