From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 tactics/elim.ml | 60 +++++++++++++++++++++++++--------------------------------
 1 file changed, 26 insertions(+), 34 deletions(-)

(limited to 'tactics/elim.ml')

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 1c7e1f0d..f2b9eec4 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -16,31 +16,23 @@ open Tacmach.New
 open Tacticals.New
 open Tactics
 open Proofview.Notations
+open Context.Named.Declaration
 
+(* Supposed to be called without as clause *)
 let introElimAssumsThen tac ba =
-  let nassums =
-    List.fold_left
-      (fun acc b -> if b then acc+2 else acc+1)
-      0 ba.Tacticals.branchsign
-  in
-  let introElimAssums = tclDO nassums intro in
+  assert (ba.Tacticals.branchnames == []);
+  let introElimAssums = tclDO ba.Tacticals.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.Tacticals.branchsign)
-  in
-  let n1 = List.length case_thin_sign in
+(* Supposed to be called with a non-recursive scheme *)
+let introCaseAssumsThen with_evars tac ba =
+  let n1 = List.length ba.Tacticals.branchsign in
   let n2 = List.length ba.Tacticals.branchnames in
   let (l1,l2),l3 =
     if n1 < n2 then List.chop n1 ba.Tacticals.branchnames, []
-    else
-      (ba.Tacticals.branchnames, []),
-       if n1 > n2 then snd (List.chop n2 case_thin_sign) else [] in
+    else (ba.Tacticals.branchnames, []), List.make (n1-n2) false in
   let introCaseAssums =
-    tclTHEN (intro_patterns l1) (intros_clearing l3) in
+    tclTHEN (intro_patterns with_evars l1) (intros_clearing l3) in
   (tclTHEN introCaseAssums (case_on_ba (tac l2) ba))
 
 (* The following tactic Decompose repeatedly applies the
@@ -71,7 +63,7 @@ and general_decompose_aux recognizer id =
   elimHypThen
     (introElimAssumsThen
        (fun bas ->
-	  tclTHEN (Proofview.V82.tactic (clear [id]))
+	  tclTHEN (clear [id])
 	    (tclMAP (general_decompose_on_hyp recognizer)
                (ids_of_named_context bas.Tacticals.assums))))
     id
@@ -84,20 +76,20 @@ 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 ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let type_of = pf_unsafe_type_of gl in
   let typc = type_of c in
   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) ]
-  end
+	      (fun id -> clear [id])));
+       exact_no_check c ]
+  end }
 
 let head_in indl t gl =
   let env = Proofview.Goal.env gl in
-  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Tacmach.New.project gl in
   try
     let ity,_ =
       if !up_to_delta
@@ -107,10 +99,10 @@ let head_in indl t gl =
   with Not_found -> false
 
 let decompose_these c l =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let indl = List.map (fun x -> x, Univ.Instance.empty) l in
   general_decompose (fun (_,t) -> head_in indl t gl) c
-  end
+  end }
 
 let decompose_and c =
   general_decompose
@@ -138,7 +130,7 @@ let induction_trailer abs_i abs_j bargs =
     (tclDO (abs_j - abs_i) intro)
     (onLastHypId
        (fun id ->
-          Proofview.Goal.nf_enter begin fun gl ->
+          Proofview.Goal.nf_enter { enter = begin fun gl ->
 	  let idty = pf_unsafe_type_of gl (mkVar id) in
 	  let fvty = global_vars (pf_env gl) idty in
 	  let possible_bring_hyps =
@@ -146,7 +138,8 @@ let induction_trailer abs_i abs_j bargs =
           in
 	  let (hyps,_) =
             List.fold_left
-	      (fun (bring_ids,leave_ids) (cid,_,_ as d) ->
+	      (fun (bring_ids,leave_ids) d ->
+                 let cid = get_id d in
                  if not (List.mem cid leave_ids)
                  then (d::bring_ids,leave_ids)
                  else (bring_ids,cid::leave_ids))
@@ -154,15 +147,14 @@ let induction_trailer abs_i abs_j bargs =
 	  in
           let ids = List.rev (ids_of_named_context hyps) in
 	  (tclTHENLIST
-            [bring_hyps hyps; tclTRY (Proofview.V82.tactic (clear ids));
-	     simple_elimination (mkVar id)])
-          end
+            [revert ids; simple_elimination (mkVar id)])
+          end }
           ))
 
 let double_ind h1 h2 =
-  Proofview.Goal.nf_enter begin fun gl ->
-  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
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let abs_i = depth_of_quantified_hypothesis true h1 gl in
+  let abs_j = 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
@@ -173,7 +165,7 @@ let double_ind h1 h2 =
        	(fun id ->
            elimination_then
              (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id))))
-  end
+  end }
 
 let h_double_induction = double_ind
 
-- 
cgit v1.2.3