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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

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 -> 
-- 
cgit v1.2.3