From 0625a1e62f070eb4d13235407eec0b818246b8b9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 28 Apr 2006 07:33:33 +0000
Subject: Typo dans précédent commit (8755); protection renforcée dans analyse
 clause in du cases

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8757 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 2 +-
 pretyping/cases.ml     | 5 ++++-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1e8c7fdef0..98919082df 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -963,7 +963,7 @@ let internalise sigma globalenv env allow_soapp lvar c =
 	      if List.exists ((<>) Anonymous) parnal then
 		user_err_loc (loc,"",
 		  str "The parameters of inductive type must be implicit");
-	      (loc,ind,nparams,nal)
+	      (loc,ind,nparams,realnal)
 	  | _ -> error_bad_inductive_type (loc_of_rawconstr t) in
 	nal, Some indsign
     | None -> 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index f709ab450e..39b26a2b70 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1546,8 +1546,11 @@ let extract_arity_signature env0 tomatchl tmsign =
 	  let realnal =
 	    match t with
 	      | Some (loc,ind',nparams,realnal) ->
-		  if ind <> ind' or List.length params <> nparams then
+		  if ind <> ind' then
 		    user_err_loc (loc,"",str "Wrong inductive type");
+		  if List.length params <> nparams
+		    or nrealargs <> List.length realnal then
+		      anomaly "Ill-formed 'in' clause in cases";
 		  List.rev realnal
 	      | None -> list_tabulate (fun _ -> Anonymous) nrealargs in
 	  let arsign = fst (get_arity env0 indf') in
-- 
cgit v1.2.3