From f83572bc45b9ab6b72688eb22d125896541ccf16 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 19 Sep 2001 16:55:41 +0000
Subject: Type 'sorts_family' (ex elimination_sorts) pour caractériser les
 familles des sortes (InProp, InSet, InType)

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

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index e9d83506ec..ff002230ff 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -44,11 +44,6 @@ type local_entry =
 
 (*s Inductive types (internal representation). *)
 
-type elimination_sorts = ElimOnProp | ElimOnSet | ElimOnType
-
-val elimination_of_sort : sorts -> elimination_sorts
-val sort_of_elimination : elimination_sorts -> sorts
-
 type recarg = 
   | Param of int 
   | Norec 
@@ -70,7 +65,7 @@ type one_inductive_body = {
   mind_user_arity : types option;
   mind_sort : sorts;
   mind_nrealargs : int;
-  mind_kelim : elimination_sorts list;
+  mind_kelim : sorts_family list;
   mind_listrec : (recarg list) array;
   mind_finite : bool;
   mind_nparams : int;
-- 
cgit v1.2.3