From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 1 Feb 2009 00:54:40 +0100
Subject: Imported Upstream version 8.2~rc2+dfsg

---
 tactics/tacticals.ml | 44 +++++++++++++++++++++++++-------------------
 1 file changed, 25 insertions(+), 19 deletions(-)

(limited to 'tactics/tacticals.ml')

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 3b13d1a0..28e987fa 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacticals.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: tacticals.ml 11735 2009-01-02 17:22:31Z herbelin $ *)
 
 open Pp
 open Util
@@ -41,6 +41,7 @@ open Tacexpr
 let tclNORMEVAR      = tclNORMEVAR
 let tclIDTAC         = tclIDTAC
 let tclIDTAC_MESSAGE = tclIDTAC_MESSAGE
+let tclORELSE0       = tclORELSE0
 let tclORELSE        = tclORELSE
 let tclTHEN          = tclTHEN
 let tclTHENLIST      = tclTHENLIST
@@ -75,7 +76,7 @@ let tclIFTHENTRYELSEMUST = tclIFTHENTRYELSEMUST
 let unTAC            = unTAC
 
 (* [rclTHENSEQ [t1;..;tn] is equivalent to t1;..;tn *)
-let tclTHENSEQ = List.fold_left tclTHEN tclIDTAC
+let tclTHENSEQ = tclTHENLIST
 
 (* map_tactical f [x1..xn] = (f x1);(f x2);...(f xn) *)
 (* tclMAP f [x1..xn] = (f x1);(f x2);...(f xn) *)
@@ -88,10 +89,16 @@ let tclNTH_HYP m (tac : constr->tactic) gl =
   tac (try mkVar(let (id,_,_) = List.nth (pf_hyps gl) (m-1) in id) 
        with Failure _ -> error "No such assumption.") gl
 
+let tclNTH_DECL m tac gl =
+  tac (try List.nth (pf_hyps gl) (m-1) 
+       with Failure _ -> error "No such assumption.") gl
+
 (* apply a tactic to the last element of the signature  *)
 
 let tclLAST_HYP = tclNTH_HYP 1
 
+let tclLAST_DECL = tclNTH_DECL 1
+
 let tclLAST_NHYPS n tac gl =
   tac (try list_firstn n (pf_ids_of_hyps gl)
        with Failure _ -> error "No such assumptions.") gl
@@ -206,7 +213,7 @@ let onHyps find tac gl = tac (find gl) gl
    after id *)
 
 let afterHyp id gl =
-  fst (list_splitby (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
+  fst (list_split_at (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
     
 
 (* Create a singleton clause list with the last hypothesis from then context *)
@@ -276,6 +283,13 @@ type branch_assumptions = {
   ba        : branch_args;     (* the branch args *)
   assums    : named_context}   (* the list of assumptions introduced *)
 
+let fix_empty_or_and_pattern nv l =
+  (* 1- The syntax does not distinguish between "[ ]" for one clause with no 
+     names and "[ ]" for no clause at all *)
+  (* 2- More generally, we admit "[ ]" for any disjunctive pattern of 
+     arbitrary length *)
+  if l = [[]] then list_make nv [] else l
+
 let check_or_and_pattern_size loc names n =
   if List.length names <> n then
     if n = 1 then 
@@ -288,10 +302,11 @@ let compute_induction_names n = function
   | None ->
       Array.make n []
   | Some (loc,IntroOrAndPattern names) ->
+      let names = fix_empty_or_and_pattern n names in
       check_or_and_pattern_size loc names n;
       Array.of_list names
-  | _ ->
-      error "Unexpected introduction pattern."
+  | Some (loc,_) ->
+      user_err_loc (loc,"",str "Disjunctive/conjunctive introduction pattern expected.")
 
 let compute_construtor_signatures isrec (_,k as ity) =
   let rec analrec c recargs =
@@ -313,23 +328,14 @@ let compute_construtor_signatures isrec (_,k as ity) =
   array_map2 analrec lc lrecargs
 
 let elimination_sort_of_goal gl = 
-  match kind_of_term (hnf_type_of gl (pf_concl gl)) with 
-    | Sort s ->
-	(match s with
-	   | Prop Null -> InProp
-	   | Prop Pos -> InSet
-	   | Type _ -> InType)
-    | _        -> anomaly "goal should be a type"
+  pf_apply Retyping.get_sort_family_of gl (pf_concl gl)
 
 let elimination_sort_of_hyp id gl = 
-  match kind_of_term (hnf_type_of gl (pf_get_hyp_typ gl id)) with 
-    | Sort s ->
-	(match s with
-	   | Prop Null -> InProp
-	   | Prop Pos -> InSet
-	   | Type _ -> InType)
-    | _        -> anomaly "goal should be a type"
+  pf_apply Retyping.get_sort_family_of gl (pf_get_hyp_typ gl id)
 
+let elimination_sort_of_clause = function
+  | None -> elimination_sort_of_goal 
+  | Some id -> elimination_sort_of_hyp id
 
 (* Find the right elimination suffix corresponding to the sort of the goal *)
 (* c should be of type A1->.. An->B with B an inductive definition *)
-- 
cgit v1.2.3