From ae6c95a3755fc3a9434bcc9fdd81b7c69baa8280 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 17 Dec 2005 21:13:48 +0000
Subject: Création d'un type d'erreur RecursionSchemeError distinct de
 InductiveError et suite correction bug #1028

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

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index d12c3a213f..5237b93db7 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -28,8 +28,8 @@ open Entries
 (************************************************************************)
 (* Various well-formedness check for inductive declarations            *)
 
+(* Errors related to inductive constructions *)
 type inductive_error =
-  (* These are errors related to inductive constructions in this module *)
   | NonPos of env * constr * constr
   | NotEnoughArgs of env * constr * constr
   | NotConstructor of env * constr * constr
@@ -39,10 +39,6 @@ type inductive_error =
   | SameNamesOverlap of identifier list
   | NotAnArity of identifier
   | BadEntry
-  (* These are errors related to recursors building in Indrec *)
-  | NotAllowedCaseAnalysis of bool * sorts * inductive
-  | BadInduction of bool * identifier * sorts
-  | NotMutualInScheme
 
 exception InductiveError of inductive_error
 
-- 
cgit v1.2.3