Add toplevel commands to declare global universes and constraints.

1 files changed, 9 insertions, 4 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c8c1d0e21..9609a959b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -96,10 +96,15 @@ let ((constr_in : constr -> Dyn.t),
 let interp_universe_name evd = function
   | None -> new_univ_level_variable univ_rigid evd
   | Some s ->
-    try let level = Evd.universe_of_name evd s in
-	  evd, level
-    with Not_found -> 
-      new_univ_level_variable ~name:s univ_rigid evd
+    try
+      let id = try Id.of_string s with _ -> raise Not_found in
+      let names, _ = Universes.global_universe_names () 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_sort evd = function
   | GProp -> evd, Prop Null