From 236c1cc7c071e23c10f50617f79ad75dca1ee664 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Thu, 6 Apr 2017 16:54:15 +0200
Subject: Avoid strange shadowing of Pretyping.interp_universe_level_name

---
 pretyping/pretyping.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 15a48a6a31..df3857df0d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -223,7 +223,7 @@ let interp_universe ?loc evd = function
 	(evd', Univ.sup u (Univ.Universe.make l)))
     (evd, Univ.Universe.type0m) l
 
-let interp_universe_level loc evd = function
+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 evd (loc,s)
 
@@ -464,11 +464,10 @@ let evar_kind_of_term sigma c =
 (*************************************************************************)
 (* Main pretyping function                                               *)
 
-let interp_universe_level_name loc evd l =
-  match l with
+let interp_glob_level loc evd : Misctypes.glob_level -> _ = function
   | GProp -> evd, Univ.Level.prop
   | GSet -> evd, Univ.Level.set
-  | GType s -> interp_universe_level loc evd s
+  | GType s -> interp_level_info loc evd s
 
 let pretype_global loc rigid env evd gr us = 
   let evd, instance = 
@@ -483,7 +482,7 @@ let pretype_global loc rigid env evd gr us =
 		       (str "Universe instance should have length " ++ int len)
        else
 	 let evd, l' = List.fold_left (fun (evd, univs) l -> 
-	    let evd, l = interp_universe_level_name loc evd l in
+	    let evd, l = interp_glob_level loc evd l in
 	      (evd, l :: univs)) (evd, []) l
 	 in
 	 if List.exists (fun l -> Univ.Level.is_prop l) l' then
-- 
cgit v1.2.3


From 49890d56dce567b029f57731c6586a6749cccb52 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Thu, 6 Apr 2017 17:00:20 +0200
Subject: Factor interp_instance out of Pretyping.pretype_global

---
 pretyping/pretyping.ml | 35 ++++++++++++++++++++---------------
 1 file changed, 20 insertions(+), 15 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index df3857df0d..92be885620 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -469,27 +469,32 @@ let interp_glob_level loc evd : Misctypes.glob_level -> _ = function
   | GSet -> evd, Univ.Level.set
   | GType s -> interp_level_info loc evd s
 
+let interp_instance loc evd ~len l =
+  if len != List.length l then
+    user_err ~loc ~hdr:"pretype"
+      (str "Universe instance should have length " ++ int len)
+  else
+    let evd, l' =
+      List.fold_left
+        (fun (evd, univs) l ->
+	  let evd, l = interp_glob_level loc evd l in
+	  (evd, l :: univs)) (evd, [])
+        l
+    in
+    if List.exists (fun l -> Univ.Level.is_prop l) l' then
+      user_err ~loc ~hdr:"pretype"
+	(str "Universe instances cannot contain Prop, polymorphic" ++
+	   str " universe instances must be greater or equal to Set.");
+    evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
+
 let pretype_global loc rigid env evd gr us = 
   let evd, instance = 
     match us with
     | None -> evd, None
     | Some l -> 
        let _, ctx = Universes.unsafe_constr_of_global gr in
-       let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in
-       let len = Array.length arr in
-       if len != List.length l then
-	 user_err ~loc ~hdr:"pretype"
-		       (str "Universe instance should have length " ++ int len)
-       else
-	 let evd, l' = List.fold_left (fun (evd, univs) l -> 
-	    let evd, l = interp_glob_level loc evd l in
-	      (evd, l :: univs)) (evd, []) l
-	 in
-	 if List.exists (fun l -> Univ.Level.is_prop l) l' then
-	   user_err ~loc ~hdr:"pretype"
-		 (str "Universe instances cannot contain Prop, polymorphic" ++
-		   str " universe instances must be greater or equal to Set.");
-	 evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
+       let len = Univ.UContext.size ctx in
+       interp_instance loc evd ~len l
   in
     Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr
 
-- 
cgit v1.2.3