Merge PR #7906: universes_of_constr don't include universes of monomorphic constants

5 files changed, 8 insertions, 11 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 382d18b09..26d105ecf 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -116,9 +116,8 @@ let instance_hook k info global imps ?hook cst =
 let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype =
   let kind = IsDefinition Instance in
   let sigma =
-    let env = Global.env () in
-    let levels = Univ.LSet.union (Univops.universes_of_constr env termtype)
-                                 (Univops.universes_of_constr env term) in
+    let levels = Univ.LSet.union (Univops.universes_of_constr termtype)
+                                 (Univops.universes_of_constr term) in
     Evd.restrict_universe_context sigma levels
   in
   let uctx = Evd.check_univ_decl ~poly sigma decl in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index a8ac52846..750ed35cb 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -163,7 +163,7 @@ let do_assumptions kind nl l =
   let nf_evar c = EConstr.to_constr sigma c in
   let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) ->
       let t = nf_evar t in
-      let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in
+      let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in
       uvars, (coe,t,imps))
       Univ.LSet.empty l
   in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index f55c852c0..a8d794642 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -93,7 +93,7 @@ let interp_definition pl bl poly red_option c ctypopt =
   let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd ty) ctx) tyopt in
   (* Keep only useful universes. *)
   let uvars_fold uvars c =
-    Univ.LSet.union uvars (universes_of_constr env evd (of_constr c))
+    Univ.LSet.union uvars (universes_of_constr evd (of_constr c))
   in
   let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in
   let evd = Evd.restrict_universe_context evd uvars in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 1d1cc62de..37258c2d4 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -262,7 +262,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
     let env = Global.env() in
     let indexes = search_guard env indexes fixdecls in
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
-    let vars = Univops.universes_of_constr env (mkFix ((indexes,0),fixdecls)) in
+    let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
     let fixdecls =
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
     let evd = Evd.from_ctx ctx in
@@ -295,8 +295,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
-    let env = Global.env () in
-    let vars = Univops.universes_of_constr env (List.hd fixdecls) in
+    let vars = Univops.universes_of_constr (List.hd fixdecls) in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     let evd = Evd.from_ctx ctx in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index e0b1349f7..fa6a9adf1 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -480,10 +480,9 @@ let declare_definition prg =
   let fix_exn = Hook.get get_fix_exn () in
   let typ = nf typ in
   let body = nf body in
-  let env = Global.env () in
   let uvars = Univ.LSet.union
-      (Univops.universes_of_constr env typ)
-      (Univops.universes_of_constr env body) in
+      (Univops.universes_of_constr typ)
+      (Univops.universes_of_constr body) in
   let uctx = UState.restrict prg.prg_ctx uvars in
   let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in
   let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in