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.ml | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 7dd9aa7864..fcb45befa0 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -122,14 +122,6 @@ where
 Remark: Set (predicative) is encoded as Type(0)
 *)
 
-let set_inductive_level env s t = 
-  let sign,s' = dest_prod_assum env t in
-  if family_of_sort s <> family_of_sort (destSort s') then
-    (* This induces reductions if user_arity <> nf_arity *)
-    mkArity (sign,s)
-  else
-    t
-
 let sort_as_univ = function
 | Type u -> u
 | Prop Null -> neutral_univ
-- 
cgit v1.2.3