From 52c0bf0da05bcfce49ce5c8321e8b9ed7b3a1cb5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 20 Nov 2001 14:38:21 +0000
Subject: types vs constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2210 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/typeops.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 603e909bd4..6556b0c764 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -48,11 +48,11 @@ let assumption_of_judgment env j
 (* Prop and Set *)
 
 let judge_of_prop =
-  { uj_val = mkProp;
+  { uj_val = body_of_type mkProp;
     uj_type = mkSort type_0 }
 
 let judge_of_set =
-  { uj_val = mkSet;
+  { uj_val = body_of_type mkSet;
     uj_type = mkSort type_0 }
 
 let judge_of_prop_contents = function
@@ -63,7 +63,7 @@ let judge_of_prop_contents = function
 
 let judge_of_type u =
   let uu = super u in
-  { uj_val = mkType u;
+  { uj_val = body_of_type (mkType u);
     uj_type = mkType uu }
 
 (*s Type of a de Bruijn index. *)
-- 
cgit v1.2.3