From 0fd0903eee374f00df87f487bf2e8e2c3d9d6f6f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 9 Sep 2001 15:34:25 +0000
Subject: Préparation à la mise en place d'univers algébriques

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

(limited to 'parsing/astterm.ml')

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 194ce335ee..c2d867ec95 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -702,7 +702,7 @@ let interp_type_with_implicits sigma env impls c =
 let interp_sort = function
   | Node(loc,"PROP", []) -> Prop Null
   | Node(loc,"SET", [])  -> Prop Pos
-  | Node(loc,"TYPE", _) -> Type Univ.dummy_univ
+  | Node(loc,"TYPE", _) -> new_Type_sort ()
   | a -> user_err_loc (Ast.loc a,"interp_sort", [< 'sTR "Not a sort" >])
 
 let judgment_of_rawconstr sigma env c =
-- 
cgit v1.2.3