From dfe97724fb6034fc06b3ef693f6a3ed94733adbc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 29 Oct 2006 20:11:08 +0000
Subject: Compatibilité du polymorphisme de constantes avec les sections.
 Amélioration affichage des univers. Réparation de petits oublis du premier
 commit. Essai d'une nouvelle stratégie : si le type d'une constante est
 mentionné explicitement, la constante est monomorphe dans Type.

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

(limited to 'kernel/inductive.mli')

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 9c75829d5b..012ddae775 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -80,8 +80,6 @@ val check_cofix : env -> cofixpoint -> unit
 val type_of_inductive_knowing_parameters :
   env -> one_inductive_body -> types array -> types
 
-val set_inductive_level : env -> sorts -> types -> types
-
 val max_inductive_sort : sorts array -> universe
 
 val instantiate_universes : env -> Sign.rel_context ->
-- 
cgit v1.2.3