Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 32 insertions, 32 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index fa4a7caa..cac200f5 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: elim.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
+(* $Id$ *)
 
 open Pp
 open Util
@@ -28,12 +28,12 @@ open Genarg
 open Tacexpr
 
 let introElimAssumsThen tac ba =
-  let nassums = 
-    List.fold_left 
-      (fun acc b -> if b then acc+2 else acc+1) 
-      0 ba.branchsign 
-  in 
-  let introElimAssums = tclDO nassums intro in 
+  let nassums =
+    List.fold_left
+      (fun acc b -> if b then acc+2 else acc+1)
+      0 ba.branchsign
+  in
+  let introElimAssums = tclDO nassums intro in
   (tclTHEN introElimAssums (elim_on_ba tac ba))
 
 let introCaseAssumsThen tac ba =
@@ -41,12 +41,12 @@ let introCaseAssumsThen tac ba =
     List.flatten
       (List.map (function b -> if b then [false;true] else [false])
 	ba.branchsign)
-  in 
+  in
   let n1 = List.length case_thin_sign in
   let n2 = List.length ba.branchnames in
   let (l1,l2),l3 =
     if n1 < n2 then list_chop n1 ba.branchnames, []
-    else 
+    else
       (ba.branchnames, []),
        if n1 > n2 then snd (list_chop n2 case_thin_sign) else [] in
   let introCaseAssums =
@@ -75,9 +75,9 @@ let elimHypThen tac id gl =
   elimination_then tac ([],[]) (mkVar id) gl
 
 let rec general_decompose_on_hyp recognizer =
-  ifOnHyp recognizer (general_decompose recognizer) (fun _ -> tclIDTAC)
+  ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> tclIDTAC)
 
-and general_decompose recognizer id =
+and general_decompose_aux recognizer id =
   elimHypThen
     (introElimAssumsThen
        (fun bas ->
@@ -93,12 +93,12 @@ and general_decompose recognizer id =
 let tmphyp_name = id_of_string "_TmpHyp"
 let up_to_delta = ref false (* true *)
 
-let general_decompose recognizer c gl = 
-  let typc = pf_type_of gl c in  
-  tclTHENSV (cut typc) 
+let general_decompose recognizer c gl =
+  let typc = pf_type_of gl c in
+  tclTHENSV (cut typc)
     [| tclTHEN (intro_using tmphyp_name)
-         (onLastHyp
-	    (ifOnHyp recognizer (general_decompose recognizer)
+         (onLastHypId
+	    (ifOnHyp recognizer (general_decompose_aux recognizer)
 	      (fun id -> clear [id])));
        exact_no_check c |] gl
 
@@ -110,7 +110,7 @@ let head_in gls indl t =
       else extract_mrectype t
     in List.mem ity indl
   with Not_found -> false
-       
+
 let inductive_of = function
   | IndRef ity -> ity
   | r ->
@@ -118,34 +118,34 @@ let inductive_of = function
         (Printer.pr_global r ++ str " is not an inductive type.")
 
 let decompose_these c l gls =
-  let indl = (*List.map inductive_of*) l in 
+  let indl = (*List.map inductive_of*) l in
   general_decompose (fun (_,t) -> head_in gls indl t) c gls
 
 let decompose_nonrec c gls =
-  general_decompose 
+  general_decompose
     (fun (_,t) -> is_non_recursive_type t)
     c gls
 
-let decompose_and c gls = 
-  general_decompose 
+let decompose_and c gls =
+  general_decompose
     (fun (_,t) -> is_record t)
     c gls
 
-let decompose_or c gls = 
-  general_decompose 
+let decompose_or c gls =
+  general_decompose
     (fun (_,t) -> is_disjunction t)
     c gls
 
 let inj_open c = (Evd.empty,c)
 
 let h_decompose l c =
-  Refiner.abstract_tactic (TacDecompose (l,inj_open c)) (decompose_these c l)
+  Refiner.abstract_tactic (TacDecompose (l,c)) (decompose_these c l)
 
 let h_decompose_or c =
-  Refiner.abstract_tactic (TacDecomposeOr (inj_open c)) (decompose_or c)
+  Refiner.abstract_tactic (TacDecomposeOr c) (decompose_or c)
 
 let h_decompose_and c =
-  Refiner.abstract_tactic (TacDecomposeAnd (inj_open c)) (decompose_and c)
+  Refiner.abstract_tactic (TacDecomposeAnd c) (decompose_and c)
 
 (* The tactic Double performs a double induction *)
 
@@ -153,17 +153,17 @@ let simple_elimination c gls =
   simple_elimination_then (fun _ -> tclIDTAC) c gls
 
 let induction_trailer abs_i abs_j bargs =
-  tclTHEN 
+  tclTHEN
     (tclDO (abs_j - abs_i) intro)
-    (onLastHyp
+    (onLastHypId
        (fun id gls ->
 	  let idty = pf_type_of gls (mkVar id) in
 	  let fvty = global_vars (pf_env gls) idty in
 	  let possible_bring_hyps =
-	    (List.tl (nLastHyps (abs_j - abs_i) gls)) @ bargs.assums
+	    (List.tl (nLastDecls (abs_j - abs_i) gls)) @ bargs.assums
           in
 	  let (hyps,_) =
-            List.fold_left 
+            List.fold_left
 	      (fun (bring_ids,leave_ids) (cid,_,cidty as d) ->
                  if not (List.mem cid leave_ids)
                  then (d::bring_ids,leave_ids)
@@ -172,7 +172,7 @@ let induction_trailer abs_i abs_j bargs =
 	  in
           let ids = List.rev (ids_of_named_context hyps) in
 	  (tclTHENSEQ
-            [bring_hyps hyps; tclTRY (clear ids); 
+            [bring_hyps hyps; tclTRY (clear ids);
 	     simple_elimination (mkVar id)])
           gls))
 
@@ -184,7 +184,7 @@ let double_ind h1 h2 gls =
     if abs_i > abs_j then (abs_j,abs_i) else
       error "Both hypotheses are the same." in
   (tclTHEN (tclDO abs_i intro)
-     (onLastHyp
+     (onLastHypId
        	(fun id ->
            elimination_then
              (introElimAssumsThen (induction_trailer abs_i abs_j))