From aa09258de6757dd38328975de2f6de7991807c68 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 10 Sep 2001 12:28:43 +0000
Subject: Utilisation d'un type spécifique (elimination_sorts) pour
 caractériser les éliminations, pour éviter les collisions avec les univers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1944 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/inductive.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/inductive.mli')

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index cb6d7b1178..e42df6d9c5 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -41,7 +41,7 @@ val mis_ntypes : inductive_instance -> int
 val mis_nconstr : inductive_instance -> int
 val mis_nparams : inductive_instance -> int
 val mis_nrealargs : inductive_instance -> int
-val mis_kelim : inductive_instance -> sorts list
+val mis_kelim : inductive_instance -> elimination_sorts list
 val mis_recargs : inductive_instance -> (recarg list) array array
 val mis_recarg : inductive_instance -> (recarg list) array
 val mis_typename : inductive_instance -> identifier
-- 
cgit v1.2.3