From 02aace9f038d579e9cf32dc2f5b21d415e977c03 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 23 Sep 2015 16:23:43 +0200
Subject: Univs (pretyping): allow parsing and decl of Top.n

This allows pretyping and detyping to be inverses regarding universes,
and makes Function's detyping/pretyping manipulations bearable in
presence of global universes that must be declared (otherwise an evd
would need to be threaded there in many places as well).
---
 pretyping/pretyping.ml | 29 +++++++++++++++++++++--------
 1 file changed, 21 insertions(+), 8 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2858a5c1fe..edb76e52f4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -102,14 +102,27 @@ let ((constr_in : constr -> Dyn.t),
 (** Miscellaneous interpretation functions *)
 let interp_universe_level_name evd s =
   let names, _ = Universes.global_universe_names () in
-  try
-    let id = try Id.of_string s with _ -> raise Not_found in
-      evd, Idmap.find id names
-  with Not_found ->
-    try let level = Evd.universe_of_name evd s in
-	  evd, level
-    with Not_found -> 
-      new_univ_level_variable ~name:s univ_rigid evd
+    if CString.string_contains s "." then
+      match List.rev (CString.split '.' s) with
+      | [] -> anomaly (str"Invalid universe name " ++ str s)
+      | n :: dp -> 
+	 let num = int_of_string n in
+	 let dp = DirPath.make (List.map Id.of_string dp) in
+	 let level = Univ.Level.make dp num in
+	 let evd =
+	   try Evd.add_global_univ evd level
+	   with Univ.AlreadyDeclared -> evd
+	 in evd, level
+    else 
+      try
+	let id =
+	  try Id.of_string s with _ -> raise Not_found in
+	  evd, Idmap.find id names
+      with Not_found ->
+	try let level = Evd.universe_of_name evd s in
+	      evd, level
+	with Not_found -> 
+	  new_univ_level_variable ~name:s univ_rigid evd
 
 let interp_universe evd = function
   | [] -> let evd, l = new_univ_level_variable univ_rigid evd in
-- 
cgit v1.2.3