Parsing of Type@{max(i,j)}.

4 files changed, 32 insertions, 26 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index bdec8307a1..3a355b91a9 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -374,9 +374,9 @@ let detype_sort = function
 	  let _, map = Universes.global_universe_names () in
 	  let pr_level u = 
 	    try Nameops.pr_id (Univ.LMap.find u map) with Not_found -> Univ.Level.pr u
-	  in
-	    Some (Pp.string_of_ppcmds (Univ.Universe.pr_with pr_level u))
-       else None)
+	  in 
+	    [Pp.string_of_ppcmds (Univ.Universe.pr_with pr_level u)]
+       else [])
 
 type binder_kind = BProd | BLambda | BLetIn
 
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index ab01065b19..5b5bbe095b 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -28,6 +28,5 @@ let smartmap_cast_type f c =
 let glob_sort_eq g1 g2 = match g1, g2 with
 | GProp, GProp -> true
 | GSet, GSet -> true
-| GType None, GType None -> true
-| GType (Some s1), GType (Some s2) -> CString.equal s1 s2
+| GType l1, GType l2 -> List.for_all2 CString.equal l1 l2
 | _ -> false
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 8557953cc4..5828e7f433 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -129,7 +129,7 @@ let pattern_of_constr sigma t =
     | Var id -> PVar id
     | Sort (Prop Null) -> PSort GProp
     | Sort (Prop Pos) -> PSort GSet
-    | Sort (Type _) -> PSort (GType None)
+    | Sort (Type _) -> PSort (GType [])
     | Cast (c,_,_)      -> pattern_of_constr c
     | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b)
     | Prod (na,c,b)   -> PProd (na,pattern_of_constr c,pattern_of_constr b)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c6a4703a08..6d98602b51 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -98,26 +98,36 @@ let ((constr_in : constr -> Dyn.t),
      (constr_out : Dyn.t -> constr)) = Dyn.create "constr"
 
 (** Miscellaneous interpretation functions *)
-
-let interp_universe_name evd = function
+let interp_universe_level_name evd s =
+  let names, _ = Universes.global_universe_names () in
+  try
+    let id = try Id.of_string s with _ -> raise Not_found 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_universe evd = function
+  | [] -> let evd, l = new_univ_level_variable univ_rigid evd in
+	    evd, Univ.Universe.make l
+  | l ->
+    List.fold_left (fun (evd, u) l -> 
+      let evd', l = interp_universe_level_name evd l in
+	(evd', Univ.sup u (Univ.Universe.make l)))
+    (evd, Univ.Universe.type0m) l
+
+let interp_universe_level evd = function
   | None -> new_univ_level_variable univ_rigid evd
-  | Some s ->
-    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
-	
+  | Some s -> interp_universe_level_name evd s
+
 let interp_sort evd = function
   | GProp -> evd, Prop Null
   | GSet -> evd, Prop Pos
   | GType n -> 
-    let evd, l = interp_universe_name evd n in
-      evd, Type (Univ.Universe.make l)
+    let evd, u = interp_universe evd n in
+      evd, Type u
 
 let interp_elimination_sort = function
   | GProp -> InProp
@@ -303,7 +313,7 @@ let evar_kind_of_term sigma c =
 let interp_universe_level_name evd = function
   | GProp -> evd, Univ.Level.prop
   | GSet -> evd, Univ.Level.set
-  | GType s -> interp_universe_name evd s
+  | GType s -> interp_universe_level evd s
 
 let pretype_global loc rigid env evd gr us = 
   let evd, instance = 
@@ -330,8 +340,6 @@ let pretype_ref loc evdref env ref us =
   | VarRef id ->
       (* Section variable *)
       (try let (_,_,ty) = lookup_named id env in
-   	   (* let ctx = Decls.variable_context id in *)
-	   (*   evdref := Evd.merge_context_set univ_rigid !evdref ctx; *)
 	     make_judge (mkVar id) ty
        with Not_found ->
          (* This may happen if env is a goal env and section variables have
@@ -345,8 +353,7 @@ let pretype_ref loc evdref env ref us =
       make_judge c ty
 
 let judge_of_Type evd s =
-  let evd, l = interp_universe_name evd s in
-  let s = Univ.Universe.make l in
+  let evd, s = interp_universe evd s in
   let judge = 
     { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
   in