Correction bug #1749 (datant de l'implantation des or-patterns) +

amélioration message d'erreur si nombre de pattern incorrect.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10427 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 13 insertions, 12 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7e288f3117..06edeaed20 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -198,7 +198,7 @@ let rec check_same_type ty1 ty2 =
   | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) ->
       List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2;
       List.iter2 (fun (_,pl1,r1) (_,pl2,r2) ->
-        List.iter2 (List.iter2 check_same_pattern) pl1 pl2;
+        List.iter2 (located_iter2 (List.iter2 check_same_pattern)) pl1 pl2;
         check_same_type r1 r2) brl1 brl2
   | CHole _, CHole _ -> ()
   | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> ()
@@ -817,7 +817,7 @@ and extern_local_binder scopes vars = function
              LocalRawAssum([(dummy_loc,na)],Default bk,ty) :: l))
 
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
-  (loc,[List.map (extern_cases_pattern_in_scope scopes vars) pl],
+  (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
    extern inctx scopes vars c)
 
 and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3214ca6c45..033052325a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -368,8 +368,7 @@ let rec has_duplicate = function
   | x::l -> if List.mem x l then (Some x) else has_duplicate l
 
 let loc_of_lhs lhs = 
- join_loc (cases_pattern_expr_loc (List.hd (List.hd lhs)))
-          (cases_pattern_expr_loc (list_last (list_last lhs)))
+ join_loc (fst (List.hd lhs)) (fst (list_last lhs))
 
 let check_linearity lhs ids =
   match has_duplicate ids with
@@ -960,15 +959,16 @@ let internalise sigma globalenv env allow_patvar lvar c =
          (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
 
   (* Expands a multiple pattern into a disjunction of multiple patterns *)
-  and intern_multiple_pattern scopes pl =
+  and intern_multiple_pattern scopes n (loc,pl) =
     let idsl_pll = 
       List.map (intern_cases_pattern globalenv scopes ([],[]) None) pl in
+    check_number_of_pattern loc n pl;
     product_of_cases_patterns [] idsl_pll
 
   (* Expands a disjunction of multiple pattern *)
-  and intern_disjunctive_multiple_pattern scopes loc mpl =
+  and intern_disjunctive_multiple_pattern scopes loc n mpl =
     assert (mpl <> []);
-    let mpl' = List.map (intern_multiple_pattern scopes) mpl in
+    let mpl' = List.map (intern_multiple_pattern scopes n) mpl in
     let (idsl,mpl') = List.split mpl' in
     let ids = List.hd idsl in
     check_or_pat_variables loc ids (List.tl idsl);
@@ -976,10 +976,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
 
   (* Expands a pattern-matching clause [lhs => rhs] *)
   and intern_eqn n (ids,tmp_scope,scopes) (loc,lhs,rhs) =
-    let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc lhs in
+    let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc n lhs in
     (* Linearity implies the order in ids is irrelevant *)
     check_linearity lhs eqn_ids;
-    check_number_of_pattern loc n (snd (List.hd pll));
     let env_ids = List.fold_right Idset.add eqn_ids ids in
     List.map (fun (subst,pl) ->
       let rhs = replace_vars_constr_expr subst rhs in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 2994bc3aea..aa3c923ebf 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -560,7 +560,7 @@ type constr_expr =
       (constr_expr * explicitation located option) list
   | CCases of loc * constr_expr option *
       (constr_expr * (name option * constr_expr option)) list *
-      (loc * cases_pattern_expr list list * constr_expr) list
+      (loc * cases_pattern_expr list located list * constr_expr) list
   | CLetTuple of loc * name list * (name option * constr_expr option) *
       constr_expr * constr_expr
   | CIf of loc * constr_expr * (name option * constr_expr option)
@@ -688,7 +688,9 @@ let rec cases_pattern_fold_names f a = function
   | CPatPrim _ | CPatAtom _ -> a
 
 let ids_of_pattern_list =
-  List.fold_left (List.fold_left (cases_pattern_fold_names Idset.add))
+  List.fold_left
+    (located_fold_left 
+      (List.fold_left (cases_pattern_fold_names Idset.add)))
     Idset.empty
 
 let rec fold_constr_expr_binders g f n acc b = function
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 608cedb3c1..fa7940faa8 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -120,7 +120,7 @@ type constr_expr =
         (constr_expr * explicitation located option) list
   | CCases of loc * constr_expr option *
       (constr_expr * (name option * constr_expr option)) list *
-      (loc * cases_pattern_expr list list * constr_expr) list
+      (loc * cases_pattern_expr list located list * constr_expr) list
   | CLetTuple of loc * name list * (name option * constr_expr option) *
       constr_expr * constr_expr
   | CIf of loc * constr_expr * (name option * constr_expr option)