Removing tactic compatibility layer from Elim.

5 files changed, 50 insertions, 54 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 5eb3dcfe6..845c4eee1 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -12,8 +12,8 @@ open Term
 open Termops
 open Inductiveops
 open Hipattern
-open Tacmach
-open Tacticals
+open Tacmach.New
+open Tacticals.New
 open Tactics
 open Misctypes
 open Proofview.Notations
@@ -22,27 +22,27 @@ let introElimAssumsThen tac ba =
   let nassums =
     List.fold_left
       (fun acc b -> if b then acc+2 else acc+1)
-      0 ba.branchsign
+      0 ba.Tacticals.branchsign
   in
-  let introElimAssums = Tacticals.New.tclDO nassums intro in
-  (Tacticals.New.tclTHEN introElimAssums (Tacticals.New.elim_on_ba tac ba))
+  let introElimAssums = tclDO nassums intro in
+  (tclTHEN introElimAssums (elim_on_ba tac ba))
 
 let introCaseAssumsThen tac ba =
   let case_thin_sign =
     List.flatten
       (List.map (function b -> if b then [false;true] else [false])
-	ba.branchsign)
+	ba.Tacticals.branchsign)
   in
   let n1 = List.length case_thin_sign in
-  let n2 = List.length ba.branchnames in
+  let n2 = List.length ba.Tacticals.branchnames in
   let (l1,l2),l3 =
-    if n1 < n2 then List.chop n1 ba.branchnames, []
+    if n1 < n2 then List.chop n1 ba.Tacticals.branchnames, []
     else
-      (ba.branchnames, []),
+      (ba.Tacticals.branchnames, []),
        if n1 > n2 then snd (List.chop n2 case_thin_sign) else [] in
   let introCaseAssums =
-    Tacticals.New.tclTHEN (intros_pattern MoveLast l1) (intros_clearing l3) in
-  (Tacticals.New.tclTHEN introCaseAssums (Tacticals.New.case_on_ba (tac l2) ba))
+    tclTHEN (intros_pattern MoveLast l1) (intros_clearing l3) in
+  (tclTHEN introCaseAssums (case_on_ba (tac l2) ba))
 
 (* The following tactic Decompose repeatedly applies the
    elimination(s) rule(s) of the types satisfying the predicate
@@ -63,18 +63,18 @@ Another example :
 *)
 
 let elimHypThen tac id =
-  Tacticals.New.elimination_then tac (mkVar id)
+  elimination_then tac (mkVar id)
 
 let rec general_decompose_on_hyp recognizer =
-  Tacticals.New.ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT())
+  ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT())
 
 and general_decompose_aux recognizer id =
   elimHypThen
     (introElimAssumsThen
        (fun bas ->
-	  Tacticals.New.tclTHEN (Proofview.V82.tactic (clear [id]))
-	    (Tacticals.New.tclMAP (general_decompose_on_hyp recognizer)
-               (ids_of_named_context bas.assums))))
+	  tclTHEN (Proofview.V82.tactic (clear [id]))
+	    (tclMAP (general_decompose_on_hyp recognizer)
+               (ids_of_named_context bas.Tacticals.assums))))
     id
 
 (* Faudrait ajouter un COMPLETE pour que l'hypothèse créée ne reste
@@ -85,17 +85,15 @@ let tmphyp_name = Id.of_string "_TmpHyp"
 let up_to_delta = ref false (* true *)
 
 let general_decompose recognizer c =
-  Proofview.Goal.enter begin fun gl ->
-  let type_of = Tacmach.New.pf_type_of gl in
-  try (* type_of can raise exceptions *)
+  Proofview.Goal.raw_enter begin fun gl ->
+  let type_of = pf_type_of gl in
   let typc = type_of c in
-  Tacticals.New.tclTHENS (cut typc)
-    [ Tacticals.New.tclTHEN (intro_using tmphyp_name)
-         (Tacticals.New.onLastHypId
-	    (Tacticals.New.ifOnHyp recognizer (general_decompose_aux recognizer)
+  tclTHENS (cut typc)
+    [ tclTHEN (intro_using tmphyp_name)
+         (onLastHypId
+	    (ifOnHyp recognizer (general_decompose_aux recognizer)
 	      (fun id -> Proofview.V82.tactic (clear [id]))));
        Proofview.V82.tactic (exact_no_check c) ]
-  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
 let head_in indl t gl =
@@ -110,7 +108,7 @@ let head_in indl t gl =
   with Not_found -> false
 
 let decompose_these c l =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
   let indl = (*List.map inductive_of*) l in
   general_decompose (fun (_,t) -> head_in indl t gl) c
   end
@@ -139,47 +137,47 @@ let h_decompose_and = decompose_and
 (* The tactic Double performs a double induction *)
 
 let simple_elimination c =
-  Tacticals.New.elimination_then (fun _ -> Tacticals.New.tclIDTAC) c
+  elimination_then (fun _ -> tclIDTAC) c
 
 let induction_trailer abs_i abs_j bargs =
-  Tacticals.New.tclTHEN
-    (Tacticals.New.tclDO (abs_j - abs_i) intro)
-    (Tacticals.New.onLastHypId
+  tclTHEN
+    (tclDO (abs_j - abs_i) intro)
+    (onLastHypId
        (fun id ->
-          Proofview.V82.tactic begin fun gls ->
-	  let idty = pf_type_of gls (mkVar id) in
-	  let fvty = global_vars (pf_env gls) idty in
+          Proofview.Goal.enter begin fun gl ->
+	  let idty = pf_type_of gl (mkVar id) in
+	  let fvty = global_vars (pf_env gl) idty in
 	  let possible_bring_hyps =
-	    (List.tl (nLastDecls (abs_j - abs_i) gls)) @ bargs.assums
+	    (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
           in
 	  let (hyps,_) =
             List.fold_left
-	      (fun (bring_ids,leave_ids) (cid,_,cidty as d) ->
+	      (fun (bring_ids,leave_ids) (cid,_,_ as d) ->
                  if not (List.mem cid leave_ids)
                  then (d::bring_ids,leave_ids)
                  else (bring_ids,cid::leave_ids))
 	      ([],fvty) possible_bring_hyps
 	  in
           let ids = List.rev (ids_of_named_context hyps) in
-	  (tclTHENSEQ
-            [Proofview.V82.of_tactic (bring_hyps hyps); tclTRY (clear ids);
-	     Proofview.V82.of_tactic (simple_elimination (mkVar id))]) gls
+	  (tclTHENLIST
+            [bring_hyps hyps; tclTRY (Proofview.V82.tactic (clear ids));
+	     simple_elimination (mkVar id)])
           end
           ))
 
 let double_ind h1 h2 =
   Proofview.Goal.enter begin fun gl ->
-  let abs_i = Tacmach.New.of_old (depth_of_quantified_hypothesis true h1) gl in
-  let abs_j = Tacmach.New.of_old (depth_of_quantified_hypothesis true h2) gl in
+  let abs_i = of_old (depth_of_quantified_hypothesis true h1) gl in
+  let abs_j = of_old (depth_of_quantified_hypothesis true h2) gl in
   let abs =
     if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else
     if abs_i > abs_j then  Proofview.tclUNIT (abs_j,abs_i) else
-      Proofview.tclZERO (Errors.UserError ("", Pp.str"Both hypotheses are the same.")) in
+      tclZEROMSG (Pp.str "Both hypotheses are the same.") in
   abs >>= fun (abs_i,abs_j) ->
-  (Tacticals.New.tclTHEN (Tacticals.New.tclDO abs_i intro)
-     (Tacticals.New.onLastHypId
+  (tclTHEN (tclDO abs_i intro)
+     (onLastHypId
        	(fun id ->
-           Tacticals.New.elimination_then
+           elimination_then
              (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id))))
   end
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 0bc96c19d..0811e229e 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -336,6 +336,9 @@ let projectAndApply thin id eqname names depids =
 	(Some (ElimOnConstr (mkVar id,NoBindings))))
     id
 
+let nLastDecls i tac =
+  Proofview.Goal.enter (fun gl -> tac (nLastDecls gl i))
+
 (* Inversion qui n'introduit pas les hypotheses, afin de pouvoir les nommer
    soi-meme (proposition de Valerie). *)
 let rewrite_equations_gene othin neqns ba =
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 926578e0e..967b6d544 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -475,14 +475,9 @@ module New = struct
       List.nth hyps (m-1)
     with Failure _ -> Errors.error "No such assumption."
 
-  let nLastDecls n tac =
-    Proofview.Goal.enter begin fun gl ->
-      let hyps =
-        try List.firstn n (Proofview.Goal.hyps gl)
-        with Failure _ -> error "Not enough hypotheses in the goal."
-      in
-      tac hyps
-    end
+  let nLastDecls gl n =
+    try List.firstn n (Proofview.Goal.hyps gl)
+    with Failure _ -> error "Not enough hypotheses in the goal."
 
   let nthHypId m gl =
     (** We only use [id] *)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index d6c9e87f9..857ced838 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -216,7 +216,7 @@ module New : sig
 
   val tclTIMEOUT : int -> unit tactic -> unit tactic
 
-  val nLastDecls  : int -> (named_context -> unit tactic) -> unit tactic
+  val nLastDecls  : [ `NF ] Proofview.Goal.t -> int -> named_context
 
   val ifOnHyp     : (identifier * types -> bool) ->
     (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 74661b836..be5b0de3a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -665,9 +665,9 @@ let apply_term hdc argl gl =
 let bring_hyps hyps =
   if List.is_empty hyps then Tacticals.New.tclIDTAC
   else
-    Proofview.Goal.enter begin fun gl ->
+    Proofview.Goal.raw_enter begin fun gl ->
       let env = Proofview.Goal.env gl in
-      let concl = Proofview.Goal.concl gl in
+      let concl = Tacmach.New.pf_nf_concl gl in
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
       let args = Array.of_list (instance_from_named_context hyps) in
       Proofview.Refine.refine begin fun h ->