From 48073edfba762df190e1b066c54e27948359497f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 9 Sep 2005 19:38:57 +0000
Subject: Suppression code inactif et commentaire apparemment incorrect (pour
 éviter confusions suite à question de CSC)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7360 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/indtypes.ml | 11 ++---------
 1 file changed, 2 insertions(+), 9 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index afff821e46..6fac5c3918 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -472,15 +472,8 @@ let allowed_sorts env issmall isunit = function
       if issmall then all_sorts
       else impredicative_sorts
   | Prop Null -> 
-(* Added InType which is derivable :when the type is unit and small *)
-(* unit+small types have all elimination 
-   In predicative system, the 
-   other inductive definitions have only Prop elimination.
-   In impredicative system, large unit type have also Set elimination
-*)   if isunit then 
-	if issmall then all_sorts
-	else if Environ.engagement env = None 
-        then logical_sorts else impredicative_sorts
+(* 29/1/02: added InType which is derivable when the type is unit and small *)
+      if isunit then all_sorts
       else logical_sorts
 
 let build_inductive env env_ar record finite inds recargs cst =
-- 
cgit v1.2.3