Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

1 files changed, 23 insertions, 14 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index eeca6301..3b13d1a0 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacticals.ml 11166 2008-06-22 13:23:35Z herbelin $ *)
+(* $Id: tacticals.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -86,7 +86,7 @@ let tclMAP tacfun l =
 
 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
+       with Failure _ -> error "No such assumption.") gl
 
 (* apply a tactic to the last element of the signature  *)
 
@@ -94,11 +94,11 @@ let tclLAST_HYP = tclNTH_HYP 1
 
 let tclLAST_NHYPS n tac gl =
   tac (try list_firstn n (pf_ids_of_hyps gl)
-       with Failure _ -> error "No such assumptions") gl
+       with Failure _ -> error "No such assumptions.") gl
 
 let tclTRY_sign (tac : constr->tactic) sign gl =
   let rec arec = function
-    | []      -> tclFAIL 0 (str "no applicable hypothesis")
+    | []      -> tclFAIL 0 (str "No applicable hypothesis.")
     | [s]     -> tac (mkVar s) (*added in order to get useful error messages *)
     | (s::sl) -> tclORELSE (tac (mkVar s)) (arec sl) 
   in 
@@ -218,7 +218,7 @@ let lastHyp gl = List.hd (pf_ids_of_hyps gl)
 
 let nLastHyps n gl =
   try list_firstn n (pf_hyps gl)
-  with Failure "firstn" -> error "Not enough hypotheses in the goal"
+  with Failure "firstn" -> error "Not enough hypotheses in the goal."
 
 
 let onClause t cls gl  = t cls gl
@@ -270,19 +270,28 @@ type branch_args = {
   nassums    : int;         (* the number of assumptions to be introduced *)
   branchsign : bool list;   (* the signature of the branch.
                                true=recursive argument, false=constant *)
-  branchnames : intro_pattern_expr list}
+  branchnames : intro_pattern_expr located list}
 
 type branch_assumptions = {
   ba        : branch_args;     (* the branch args *)
   assums    : named_context}   (* the list of assumptions introduced *)
 
+let check_or_and_pattern_size loc names n =
+  if List.length names <> n then
+    if n = 1 then 
+      user_err_loc (loc,"",str "Expects a conjunctive pattern.")
+    else 
+      user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n 
+	++ str " branches.")
+
 let compute_induction_names n = function
-  | IntroAnonymous ->
+  | None ->
       Array.make n []
-  | IntroOrAndPattern names when List.length names = n ->
+  | Some (loc,IntroOrAndPattern names) ->
+      check_or_and_pattern_size loc names n;
       Array.of_list names
   | _ ->
-      errorlabstrm "" (str "Expects " ++ int n ++ str " lists of names")
+      error "Unexpected introduction pattern."
 
 let compute_construtor_signatures isrec (_,k as ity) =
   let rec analrec c recargs =
@@ -335,7 +344,7 @@ let general_elim_then_using mk_elim
   let indmv = 
     match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
-      | _         -> error "elimination"
+      | _         -> anomaly "elimination"
   in
   let pmv =
     let p, _ = decompose_app elimclause.templtyp.Evd.rebus in
@@ -348,7 +357,7 @@ let general_elim_then_using mk_elim
 	      | Var id -> string_of_id id
 	      | _ -> "\b"
 	  in
-	  error ("The elimination combinator " ^ name_elim ^ " is not known") 
+	  error ("The elimination combinator " ^ name_elim ^ " is unknown.") 
   in
   let elimclause' = clenv_fchain indmv elimclause indclause' in
   let elimclause' = clenv_match_args elimbindings elimclause' in
@@ -393,7 +402,7 @@ let elimination_then_using tac predicate bindings c gl =
   let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
   let indclause  = mk_clenv_from gl (c,t) in
   general_elim_then_using gl_make_elim
-    true IntroAnonymous tac predicate bindings ind indclause gl
+    true None tac predicate bindings ind indclause gl
 
 let case_then_using =
   general_elim_then_using gl_make_case_dep false
@@ -423,7 +432,7 @@ let make_elim_branch_assumptions ba gl =
 		   id::constargs,
 		   recargs,
 		   indargs) tl idtl
-      | (_, _) -> error "make_elim_branch_assumptions"
+      | (_, _) -> anomaly "make_elim_branch_assumptions"
   in 
   makerec ([],[],[],[],[]) ba.branchsign
     (try list_firstn ba.nassums (pf_hyps gl)
@@ -447,7 +456,7 @@ let make_case_branch_assumptions ba gl =
 		   id::cargs,
 		   recargs,
 		   id::constargs) tl idtl
-      | (_, _) -> error "make_case_branch_assumptions"
+      | (_, _) -> anomaly "make_case_branch_assumptions"
   in 
   makerec ([],[],[],[]) ba.branchsign
     (try list_firstn ba.nassums (pf_hyps gl)