- Better parsing and printing of named universes: Type{ident} and foo@{(ident|Prop|Set|Type|' ')*}

(user given names are still write only).
- Add test-suite file for named universes.

3 files changed, 114 insertions, 4 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 69ba73c673..86fa5518cc 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -153,7 +153,7 @@ GEXTEND Gram
     [ [ "Set"  -> GSet
       | "Prop" -> GProp
       | "Type" -> GType None
-      | "Type"; "{"; id = string; "}" -> GType (Some id)
+      | "Type"; "{"; id = ident; "}" -> GType (Some (Id.to_string id))
       ] ]
   ;
   lconstr:
@@ -287,9 +287,16 @@ GEXTEND Gram
       | id=pattern_ident -> CPatVar(!@loc,(false,id)) ] ]
   ;
   instance:
-    [ [ "@{"; l = LIST1 sort SEP ","; "}" -> Some l
+    [ [ "@{"; l = LIST1 level; "}" -> Some l
       | -> None ] ]
   ;
+  level:
+    [ [ "Set" -> GSet
+      | "Prop" -> GProp
+      | "Type" -> GType None
+      | id = ident -> GType (Some (Id.to_string id))
+      ] ]
+  ;
   fix_constr:
     [ [ fx1=single_fix -> mk_single_fix fx1
       | (_,kw,dcl1)=single_fix; "with"; dcls=LIST1 fix_decl SEP "with";
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 5b6c072839..22c89af8aa 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -108,10 +108,12 @@ let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
 
 let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
 
+let pr_in_braces pr x = str "{" ++ pr x ++ str "}"
+
 let pr_glob_sort = function
   | GProp -> str "Prop"
   | GSet -> str "Set"
-  | GType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment str) u)
+  | GType u -> hov 0 (str "Type" ++ pr_opt_no_spc (pr_in_braces str) u)
 
 let pr_id = pr_id
 let pr_name = pr_name
@@ -127,7 +129,8 @@ let pr_glob_sort_instance = function
     | None -> str "Type")
 
 let pr_universe_instance l =
-  pr_opt (pr_in_comment (prlist_with_sep spc pr_glob_sort_instance)) l
+  pr_opt_no_spc (fun i -> 
+    str"@" ++ pr_in_braces (prlist_with_sep spc pr_glob_sort_instance) i) l
 
 let pr_cref ref us =
   pr_reference ref ++ pr_universe_instance us
diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v
new file mode 100644
index 0000000000..62ee5519d9
--- /dev/null
+++ b/test-suite/success/namedunivs.v
@@ -0,0 +1,100 @@
+(* Inductive paths {A} (x : A) : A -> Type := idpath : paths x x where "x = y" := (@paths _ x y) : type_scope. *)
+(* Goal forall A B : Set, @paths Type A B -> @paths Set A B. *)
+(*   intros A B H. *)
+(* Fail  exact H. *)
+(* Abort . *)
+
+Section lift_strict.
+Polymorphic Definition liftlt := 
+  let t := Type{i} : Type{k} in
+  fun A : Type{i} => A : Type{k}.
+
+Polymorphic Definition liftle := 
+  fun A : Type{i} => A : Type{k}.
+End lift_strict.
+
+
+Set Universe Polymorphism.
+
+(* Inductive option (A : Type) : Type := *)
+(*   | None : option A *)
+(*   | Some : A -> option A. *)
+
+Inductive option (A : Type{i}) : Type{i} :=
+  | None : option A
+  | Some : A -> option A.
+
+Definition foo' {A : Type{i}} (o : option@{i} A) : option@{i} A :=
+  o.
+
+Definition foo'' {A : Type{i}} (o : option@{j} A) : option@{k} A :=
+  o.
+
+(* Inductive prod (A : Type{i}) (B : Type{j}) := *)
+(*   | pair : A -> B -> prod A B. *)
+
+(* Definition snd {A : Type{i}} (B : Type{j}) (p : prod A B) : B := *)
+(*   match p with *)
+(*     | pair _ _ a b => b *)
+(*   end. *)
+
+(* Definition snd' {A : Type{i}} (B : Type{i}) (p : prod A B) : B := *)
+(*   match p with *)
+(*     | pair _ _ a b => b *)
+(*   end. *)
+
+
+(* Inductive paths {A : Type} : A -> A -> Type := *)
+(* | idpath (a : A) : paths a a. *)
+
+Inductive paths {A : Type{i}} : A -> A -> Type{i} :=
+| idpath (a : A) : paths a a.
+
+Definition Funext := 
+  forall (A : Type) (B : A -> Type),
+  forall f g : (forall a, B a), (forall x : A, paths (f x) (g x)) -> paths f g.
+
+Definition paths_lift_closed (A : Type{i}) (x y : A) :
+  paths x y -> @paths (liftle@{j Type} A) x y.
+Proof. 
+  intros. destruct X. exact (idpath _).
+Defined.
+
+Definition paths_lift (A : Type{i}) (x y : A) :
+  paths x y -> paths@{j} x y.
+Proof. 
+  intros. destruct X. exact (idpath _).
+Defined.
+
+Definition paths_lift_closed_strict (A : Type{i}) (x y : A) :
+  paths x y -> @paths (liftlt@{j Type} A) x y.
+Proof. 
+  intros. destruct X. exact (idpath _).
+Defined.
+
+Definition paths_downward_closed_le (A : Type{i}) (x y : A) :
+  paths@{j} (A:=liftle@{i j} A) x y -> paths@{i} x y.
+Proof. 
+  intros. destruct X. exact (idpath _).
+Defined.
+
+Definition paths_downward_closed_lt (A : Type{i}) (x y : A) :
+  @paths (liftlt@{j i} A) x y -> paths x y.
+Proof. 
+  intros. destruct X. exact (idpath _).
+Defined.
+
+Definition paths_downward_closed_lt_nolift (A : Type{i}) (x y : A) :
+  paths@{j} x y -> paths x y.
+Proof. 
+  intros. destruct X. exact (idpath _).
+Defined.
+
+Definition funext_downward_closed (F : Funext@{i' j' k'}) :
+  Funext@{i j k}. 
+Proof.
+  intros A B f g H. red in F.
+  pose (F A B f g (fun x => paths_lift _ _ _ (H x))).
+  apply paths_downward_closed_lt_nolift. apply p.
+Defined.
+