From ad74cfff28ffc9e82cb14d189761cf9c776ab09d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 5 May 2005 10:39:44 +0000
Subject: Code v7 obsolete

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6993 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/univ.mli    | 2 --
 parsing/termast.ml | 1 -
 2 files changed, 3 deletions(-)

diff --git a/kernel/univ.mli b/kernel/univ.mli
index 990460f9bb..56442cbccd 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -52,8 +52,6 @@ val merge_constraints : constraints -> universes -> universes
 val pr_uni : universe -> Pp.std_ppcmds
 val pr_universes : universes -> Pp.std_ppcmds
 
-val string_of_univ : universe -> string
-
 (*s Dumping to a file *)
 
 val dump_universes : out_channel -> universes -> unit
diff --git a/parsing/termast.ml b/parsing/termast.ml
index ace1b47d20..b4871598d0 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -342,7 +342,6 @@ let rec ast_of_raw = function
       (match s with
 	 | RProp Null -> ope("PROP",[])
 	 | RProp Pos -> ope("SET",[])
-	 | RType (Some u) when !print_universes -> ope("TYPE",[ide(Univ.string_of_univ u)])
 	 | RType _ -> ope("TYPE",[]))
   | RHole _ -> ope("ISEVAR",[])
   | RCast (_,c,t) -> ope("CAST",[ast_of_raw c;ast_of_raw t])
-- 
cgit v1.2.3