Merge PR #1033: Universe binder improvements

3 files changed, 37 insertions, 31 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index eb90e5fe0..00c254dbe 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -177,13 +177,20 @@ let _ =
 	    optwrite = (:=) Universes.set_minimization })
 
 (** Miscellaneous interpretation functions *)
+let interp_known_universe_level evd id =
+  try
+    let level = Evd.universe_of_name evd id in
+    level
+  with Not_found ->
+    let names, _ = Global.global_universe_names () in
+    snd (Id.Map.find id names)
+
 let interp_universe_level_name ~anon_rigidity evd (loc, s) =
   match s with
   | Anonymous ->
      new_univ_level_variable ?loc anon_rigidity evd
-  | Name s ->
-     let s = Id.to_string s in
-     let names, _ = Global.global_universe_names () in
+  | Name id ->
+     let s = Id.to_string id in
      if CString.string_contains ~where:s ~what:"." then
        match List.rev (CString.split '.' s) with
        | [] -> anomaly (str"Invalid universe name " ++ str s ++ str".")
@@ -196,18 +203,12 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) =
 	    with UGraph.AlreadyDeclared -> evd
 	  in evd, level
      else
-       try
-	 let level = Evd.universe_of_name evd s in
-	 evd, level
+       try evd, interp_known_universe_level evd id
        with Not_found ->
-	 try
-	   let id = try Id.of_string s with _ -> raise Not_found in
-           evd, snd (Id.Map.find id names)
-	 with Not_found ->
-	   if not (is_strict_universe_declarations ()) then
-  	     new_univ_level_variable ?loc ~name:s univ_rigid evd
-	   else user_err ?loc ~hdr:"interp_universe_level_name"
-		  (Pp.(str "Undeclared universe: " ++ str s))
+         if not (is_strict_universe_declarations ()) then
+           new_univ_level_variable ?loc ~name:id univ_rigid evd
+         else user_err ?loc ~hdr:"interp_universe_level_name"
+             (Pp.(str "Undeclared universe: " ++ str s))
 
 let interp_universe ?loc evd = function
   | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
@@ -219,6 +220,15 @@ let interp_universe ?loc evd = function
 	(evd', Univ.sup u (Univ.Universe.make l)))
     (evd, Univ.Universe.type0m) l
 
+let interp_known_level_info ?loc evd = function
+  | None | Some (_, Anonymous) ->
+    user_err ?loc ~hdr:"interp_known_level_info"
+      (str "Anonymous universes not allowed here.")
+  | Some (loc, Name id) ->
+    try interp_known_universe_level evd id
+    with Not_found ->
+      user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Id.print id)
+
 let interp_level_info ?loc evd : Misctypes.level_info -> _ = function
   | None -> new_univ_level_variable ?loc univ_rigid evd
   | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s)
@@ -467,6 +477,11 @@ let pretype_id pretype k0 loc env evdref lvar id =
 (*************************************************************************)
 (* Main pretyping function                                               *)
 
+let interp_known_glob_level ?loc evd = function
+  | GProp -> Univ.Level.prop
+  | GSet -> Univ.Level.set
+  | GType s -> interp_known_level_info ?loc evd s
+
 let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function
   | GProp -> evd, Univ.Level.prop
   | GSet -> evd, Univ.Level.set
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 838938524..fe10be9e7 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -20,6 +20,9 @@ open Glob_term
 open Ltac_pretype
 open Evardefine
 
+val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
+  Misctypes.glob_level -> Univ.Level.t
+
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
 val search_guard :
diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml
index 5576e33f4..3cf32d7ff 100644
--- a/pretyping/univdecls.ml
+++ b/pretyping/univdecls.ml
@@ -6,9 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-open CErrors
 open Names
+open CErrors
 
 (** Local universes and constraints declarations *)
 type universe_decl =
@@ -22,27 +21,16 @@ let default_univ_decl =
     univdecl_extensible_constraints = true }
 
 let interp_univ_constraints env evd cstrs =
-  let open Misctypes in
-  let u_of_id x =
-    match x with
-    | Misctypes.GProp -> Loc.tag Univ.Level.prop
-    | GSet  -> Loc.tag Univ.Level.set
-    | GType None | GType (Some (_, Anonymous)) ->
-       user_err ~hdr:"interp_constraint"
-                     (str "Cannot declare constraints on anonymous universes")
-    | GType (Some (loc, Name id)) ->
-       try loc, Evd.universe_of_name evd (Id.to_string id)
-       with Not_found ->
-         user_err ?loc ~hdr:"interp_constraint" (str "Undeclared universe " ++ Id.print id)
-  in
   let interp (evd,cstrs) (u, d, u') =
-    let lloc, ul = u_of_id u and rloc, u'l = u_of_id u' in
+    let ul = Pretyping.interp_known_glob_level evd u in
+    let u'l = Pretyping.interp_known_glob_level evd u' in
     let cstr = (ul,d,u'l) in
     let cstrs' = Univ.Constraint.add cstr cstrs in
     try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
         evd, cstrs'
     with Univ.UniverseInconsistency e ->
-      user_err  ~hdr:"interp_constraint" (str "Universe inconsistency" (* TODO *))
+      user_err ~hdr:"interp_constraint"
+        (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
   in
   List.fold_left interp (evd,Univ.Constraint.empty) cstrs