Insertion automatique des motifs de let-in s'il ne sont pas explicitement mentionnés (pour compatibilité)

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

1 files changed, 21 insertions, 7 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ac9777a14..42569c9ce 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -480,14 +480,27 @@ let pattern_status pats =
 (* Well-formedness tests *)
 (* Partial check on patterns *)
 
-let check_constructor loc (_,j as cstr_sp) mind cstrs args =
+exception NotAdjustable
+
+let rec adjust_local_defs = function
+  | (pat :: pats, (_,None,_) :: decls) ->
+      pat :: adjust_local_defs (pats,decls)
+  | (pats, (_,Some _,_) :: decls) ->
+      PatVar (dummy_loc, Anonymous) :: adjust_local_defs (pats,decls)
+  | [], [] -> []
+  | _ -> raise NotAdjustable
+
+let check_and_adjust_constructor loc (_,j as cstr_sp) mind cstrs pats =
   (* Check it is constructor of the right type *)
   if inductive_of_constructor cstr_sp <> mind
   then error_bad_constructor_loc loc cstr_sp mind;
   (* Check the constructor has the right number of args *)
-  let nb_args_constr = cstrs.(j-1).cs_nargs in 
-  if List.length args <> nb_args_constr
-  then error_wrong_numarg_constructor_loc loc cstr_sp nb_args_constr
+  let nb_args_constr = cstrs.(j-1).cs_nargs in
+  if List.length pats = nb_args_constr then pats
+  else
+    try adjust_local_defs (pats, cstrs.(j-1).cs_args)
+    with NotAdjustable ->
+      error_wrong_numarg_constructor_loc loc cstr_sp nb_args_constr
 
 let check_all_variables typ mat =
   List.iter
@@ -1038,11 +1051,12 @@ let group_equations mind current cstrs mat =
 		 let rest = {rest with tag = lower_pattern_status rest.tag} in
 		 brs.(i-1) <- (args, rest) :: brs.(i-1)
 	       done
-	   | PatCstr(loc,((ind_sp,i) as cstr),largs,alias) ->
+	   | PatCstr(loc,((_,i) as cstr),args,alias) ->
 	       (* This is a regular clause *)
-	       check_constructor loc cstr mind cstrs largs;
+	       let args' =
+		 check_and_adjust_constructor loc cstr mind cstrs args in
 	       only_default := false;
-	       brs.(i-1) <- (largs,rest) :: brs.(i-1)) mat () in
+	       brs.(i-1) <- (args',rest) :: brs.(i-1)) mat () in
   (brs,!only_default)
 
 (************************************************************************)