Towards unifying parsing/printing for universe instances and Type's argument.

We consistently use:
- UUnknown: to mean a rigid anonymous universe
  (written Type in instances and Type as a sort)
  [was formerly encoded as [] in Type's argument]
- UAnonymous: to mean a flexible anonymous universe
  (written _ in instances and Type@{_} as a sort)
  [was formerly encoded as [None] in Type's argument]
- UNamed: to mean a named universe or universe expression
  (written id or qualid in instances and Type@{id} or Type@{qualid} or more
   generally Type@{id+n}, Type@{qualid+n}, Type@{max(...)} as a sort)

There is a little change of syntax: "_" in a "max" list of universes
(e.g. "Type@{max(_,id+1)}" is not anymore allowed. But it was
trivially satisfiable by unifying the flexible universe with a
neighbor of the list and the syntax is anyway not documented.

There is a little change of semantics: if I do id@{Type} for an
abbreviation "id := Type", it will consider a rigid variable rather
than a flexible variable as before.

2 files changed, 10 insertions, 12 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fe50bd4b08..c05af8be45 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -757,11 +757,9 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo
 (* mapping glob_constr to constr_expr                                    *)
 
 let extern_glob_sort = function
-  | GSProp -> GSProp
-  | GProp -> GProp
-  | GSet -> GSet
-  | GType _ as s when !print_universes -> s
-  | GType _ -> GType []
+  (* In case we print a glob_constr w/o having passed through detyping *)
+  | GType _ when not !print_universes -> GType UUnknown
+  | u -> u
 
 let extern_universes = function
   | Some _ as l when !print_universes -> l
@@ -1315,7 +1313,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
   | PSort Sorts.InSProp -> GSort GSProp
   | PSort Sorts.InProp -> GSort GProp
   | PSort Sorts.InSet -> GSort GSet
-  | PSort Sorts.InType -> GSort (GType [])
+  | PSort Sorts.InType -> GSort (GType UUnknown)
   | PInt i -> GInt i
 
 let extern_constr_pattern env sigma pat =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1dd68f2abf..b4294b4ff8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -998,18 +998,18 @@ let intern_reference qid =
   in
   Smartlocate.global_of_extended_global r
 
-let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option =
+let sort_info_of_level_info (info: level_info) : sort_info =
   match info with
-  | UAnonymous -> None
-  | UUnknown -> None
-  | UNamed id -> Some (id, 0)
+  | UAnonymous -> UAnonymous
+  | UUnknown -> UUnknown
+  | UNamed id -> UNamed [id,0]
 
 let glob_sort_of_level (level: glob_level) : glob_sort =
   match level with
   | GSProp -> GSProp
   | GProp -> GProp
   | GSet -> GSet
-  | GType info -> GType [sort_info_of_level_info info]
+  | GType info -> GType (sort_info_of_level_info info)
 
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
@@ -1045,7 +1045,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
           DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg)
         | _ -> err ()
         end
-      | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
+      | Some [s], GSort (GType UUnknown) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
       | Some [_old_level], GSort _new_sort ->
         (* TODO: add old_level and new_sort to the error message *)
         user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid)