From 72de7e057505c45cdbf75234a9ea90465d0e19ec Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 13:15:06 +0200
Subject: Simplify fresh_foo_instance functions and pretyping of univ instance

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

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 495f5c0660..f2881e4a19 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -405,32 +405,25 @@ let interp_glob_level ?loc evd : 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
+let interp_instance ?loc evd l =
+  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 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')))
+      (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 = Global.constr_of_global_in_context !!env gr in
-       let len = Univ.AUContext.size ctx in
-       interp_instance ?loc evd ~len l
+    | Some l -> interp_instance ?loc evd l
   in
   Evd.fresh_global ?loc ~rigid ?names:instance !!env evd gr
 
-- 
cgit v1.2.3


From 5993c266300cca1c7ca6e8b2b8e3f77f745ca9f9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 13:27:27 +0200
Subject: Simplify vars_of_global usage

---
 pretyping/evarsolve.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 62d719034c..22f438c00c 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -457,7 +457,7 @@ let free_vars_and_rels_up_alias_expansion env sigma aliases c =
         | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
         | _ -> frec (aliases,depth) c end
     | Const _ | Ind _ | Construct _ ->
-        acc2 := Id.Set.union (vars_of_global env (EConstr.to_constr sigma c)) !acc2
+        acc2 := Id.Set.union (vars_of_global env (fst @@ EConstr.destRef sigma c)) !acc2
     | _ ->
         iter_with_full_binders sigma
           (fun d (aliases,depth) -> (extend_alias sigma d aliases,depth+1))
-- 
cgit v1.2.3


From 5bf063c15468bb81f0f48b583f600250cd829aee Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 13:37:46 +0200
Subject: UnivGen.constr_of_glob_univ -> Constr.mkRef

---
 pretyping/typeclasses.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 7e5815acd1..ce12aaeeb0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -320,7 +320,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
 	    hints @ (path', info, body) :: rest
 	in List.fold_left declare_proj [] projs 
   in
-  let term = UnivGen.constr_of_global_univ (glob, inst) in
+  let term = Constr.mkRef (glob, inst) in
     (*FIXME subclasses should now get substituted for each particular instance of
       the polymorphic superclass *)
     aux pri term ty [glob]
-- 
cgit v1.2.3