From 18ef44c722b7d72ba67d02d4127e708fc237c089 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Sun, 5 Dec 1999 18:34:26 +0000
Subject: explicitations erreurs inductifs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@203 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/inductive.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 0e8dc75d2a..9dc0ca3659 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -74,10 +74,10 @@ type mutual_inductive_entry = {
   mind_entry_inds : (identifier * constr * identifier list * constr) list }
 
 type inductive_error =
-  | NonPos of int   
-  | NotEnoughArgs of int
-  | NotConstructor  
-  | NonPar of int * int
+  | NonPos of name list * constr * constr
+  | NotEnoughArgs of name list * constr * constr
+  | NotConstructor of name list * constr * constr
+  | NonPar of name list * constr * int * constr * constr
   | SameNamesTypes of identifier
   | SameNamesConstructors of identifier * identifier
   | NotAnArity of identifier
@@ -125,7 +125,7 @@ let mind_extract_params = decompose_prod_n
   
 let extract nparams c =
   try mind_extract_params nparams c 
-  with UserError _ -> raise (InductiveError (NotEnoughArgs nparams))
+  with UserError _ -> raise (InductiveError BadEntry)
 
 let check_params nparams params c = 
   if not (fst (extract nparams c) = params) then 
-- 
cgit v1.2.3