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 +-
 tactics/equality.ml | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

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 =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 484a17c2f2..9d623fe51e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -435,8 +435,9 @@ let construct_discriminator sigma env dirn c sort =
   let arsign,arsort = get_arity indf in
   let (true_0,false_0,sort_0) = 
     match necessary_elimination arsort (destSort sort) with
-      | Type_Type -> build_coq_UnitT (), build_coq_EmptyT (), (Type dummy_univ)
-      | _         -> build_coq_True (),  build_coq_False (),  (Prop Null)
+      | Type_Type ->
+	  build_coq_UnitT (), build_coq_EmptyT (), Evarutil.new_Type_sort ()
+      | _         -> build_coq_True (),  build_coq_False (), (Prop Null)
   in
   let p = it_mkLambda_or_LetIn (mkSort sort_0) arsign in
   let cstrs = get_constructors indf in
@@ -462,8 +463,7 @@ let rec build_discriminator sigma env dirn c sort = function
       let newc = mkRel(cnum_nlams-(argnum-nparams)) in
       let subval = build_discriminator sigma cnum_env dirn newc sort l  in
       (match necessary_elimination arsort (destSort sort) with
-         | Type_Type ->
-	     kont subval (build_coq_EmptyT (),mkSort (Type(dummy_univ)))
+         | Type_Type -> kont subval (build_coq_EmptyT (),Evarutil.new_Type ())
 	 | _ -> kont subval (build_coq_False (),mkSort (Prop Null)))
 
 let find_eq_data_decompose eqn =
-- 
cgit v1.2.3