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.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/inductive.mli')

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 8140d949d7..1f1d5927fa 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -75,10 +75,10 @@ type mutual_inductive_entry = {
   definition. *)
 
 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
-- 
cgit v1.2.3