From a98cbb0391769b2904a8127d73cbb731521e8fce Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 8 Nov 2003 09:53:47 +0000
Subject: Suppression StronglyClassical, StronglyConstructive devient plus
 concretement ImpredicativeSet

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

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 96e3cabd42..46ee8d97e1 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -198,7 +198,7 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        if engagement env = Some StronglyConstructive then
+        if engagement env = Some ImpredicativeSet then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
         else
-- 
cgit v1.2.3