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, 3 insertions, 3 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 4c67d65816..889a2d7359 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1302,7 +1302,7 @@ let rec rebuild_return_type rt =
 	CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
     | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous],
                                        Constrexpr.Default Decl_kinds.Explicit, rt)],
-			    CAst.make @@ Constrexpr.CSort(GType []))
+                            CAst.make @@ Constrexpr.CSort(GType UUnknown))
 
 let do_build_inductive
       evd (funconstants: pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 56f17703ff..4470c36888 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -194,7 +194,7 @@ let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args)
 let mkRVar id = DAst.make @@ GRef (VarRef id,None)
 let mkRltacVar id = DAst.make @@ GVar (id)
 let mkRCast rc rt =  DAst.make @@ GCast (rc, CastConv rt)
-let mkRType =  DAst.make @@ GSort (GType [])
+let mkRType =  DAst.make @@ GSort (GType UUnknown)
 let mkRProp =  DAst.make @@ GSort (GProp)
 let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, Explicit, rt1, rt2)
 let mkRConstruct c = DAst.make @@ GRef (ConstructRef c,None)
@@ -872,7 +872,7 @@ open Util
 
 (** Constructors for constr_expr *)
 let mkCProp loc = CAst.make ?loc @@ CSort GProp
-let mkCType loc = CAst.make ?loc @@ CSort (GType [])
+let mkCType loc = CAst.make ?loc @@ CSort (GType UUnknown)
 let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)
 let rec mkCHoles ?loc n =
   if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)