Pick the universe graph out of the environment in conversion API.

7 files changed, 27 insertions, 27 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 5873d1f502..c7b866179b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -80,12 +80,11 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
               let j = Typeops.infer env' c in
               assert (j.uj_val == c); (* relevances should already be correct here *)
               let typ = cb.const_type in
-              let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
-                  j.uj_type typ in
+              let cst' = Reduction.infer_conv_leq env' j.uj_type typ in
               j.uj_val, cst'
             | Def cs ->
               let c' = Mod_subst.force_constr cs in
-              c, Reduction.infer_conv env' (Environ.universes env') c c'
+              c, Reduction.infer_conv env' c c'
             | Primitive _ ->
               error_incorrect_with_constraint lab
           in
@@ -103,12 +102,11 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
               let j = Typeops.infer env' c in
               assert (j.uj_val == c); (* relevances should already be correct here *)
               let typ = cb.const_type in
-              let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
-                  j.uj_type typ in
+              let cst' = Reduction.infer_conv_leq env' j.uj_type typ in
               cst'
             | Def cs ->
               let c' = Mod_subst.force_constr cs in
-              let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in
+              let cst' = Reduction.infer_conv env' c c' in
               cst'
             | Primitive _ ->
               error_incorrect_with_constraint lab
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 3543168175..fc6afb79d4 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -150,10 +150,10 @@ let warn_no_native_compiler =
          (fun () -> strbrk "Native compiler is disabled," ++
                       strbrk " falling back to VM conversion test.")
 
-let native_conv_gen pb sigma env graph univs t1 t2 =
+let native_conv_gen pb sigma env univs t1 t2 =
   if not (typing_flags env).Declarations.enable_native_compiler then begin
     warn_no_native_compiler ();
-    Vconv.vm_conv_gen pb env graph univs t1 t2
+    Vconv.vm_conv_gen pb env univs t1 t2
   end
   else
   let ml_filename, prefix = get_ml_filename () in
@@ -179,4 +179,4 @@ let native_conv cv_pb sigma env t1 t2 =
     let state = (univs, checked_universes) in
     let t1 = Term.it_mkLambda_or_LetIn t1 (Environ.rel_context env) in
     let t2 = Term.it_mkLambda_or_LetIn t2 (Environ.rel_context env) in
-    let _ = native_conv_gen cv_pb sigma env univs state t1 t2 in ()
+    let _ = native_conv_gen cv_pb sigma env state t1 t2 in ()
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b572a39047..8258c1c086 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -219,9 +219,9 @@ type 'a universe_compare = {
 
 type 'a universe_state = 'a * 'a universe_compare
 
-type ('a,'b) generic_conversion_function = env -> UGraph.t -> 'b universe_state -> 'a -> 'a -> 'b
+type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b
 
-type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
+type 'a infer_conversion_function = env -> 'a -> 'a -> Univ.Constraint.t
 
 let sort_cmp_universes env pb s0 s1 (u, check) =
   (check.compare_sorts env pb s0 s1 u, check)
@@ -899,12 +899,14 @@ let conv = gen_conv CONV
 
 let conv_leq = gen_conv CUMUL
 
-let generic_conv cv_pb ~l2r evars reds env graph univs t1 t2 =
+let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
+  let graph = Environ.universes env in
   let (s, _) =
     clos_gen_conv reds cv_pb l2r evars env graph univs t1 t2
   in s
 
-let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
+let infer_conv_universes cv_pb l2r evars reds env t1 t2 =
+  let univs = Environ.universes env in
   let b, cstrs =
     if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2
     else Constr.eq_constr_univs_infer univs t1 t2
@@ -919,16 +921,16 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
 let infer_conv_universes =
   if Flags.profile then
     let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in
-      CProfile.profile8 infer_conv_universes_key infer_conv_universes
+      CProfile.profile7 infer_conv_universes_key infer_conv_universes
   else infer_conv_universes
 
 let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
-    env univs t1 t2 =
-  infer_conv_universes CONV l2r evars ts env univs t1 t2
+    env t1 t2 =
+  infer_conv_universes CONV l2r evars ts env t1 t2
 
 let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
-    env univs t1 t2 =
-  infer_conv_universes CUMUL l2r evars ts env univs t1 t2
+    env t1 t2 =
+  infer_conv_universes CUMUL l2r evars ts env t1 t2
 
 let default_conv cv_pb ?l2r:_ env t1 t2 =
     gen_conv cv_pb env t1 t2
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 0027b7bf47..3c747f0ff8 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -46,9 +46,9 @@ type 'a universe_compare = {
 
 type 'a universe_state = 'a * 'a universe_compare
 
-type ('a,'b) generic_conversion_function = env -> UGraph.t -> 'b universe_state -> 'a -> 'a -> 'b
+type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b
 
-type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
+type 'a infer_conversion_function = env -> 'a -> 'a -> Univ.Constraint.t
 
 val get_cumulativity_constraints : conv_pb -> Univ.Variance.t array ->
   Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 28baa82666..76a1c190be 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -85,7 +85,7 @@ let make_labmap mp list =
 
 let check_conv_error error why cst poly f env a1 a2 =
   try
-    let cst' = f env (Environ.universes env) a1 a2 in
+    let cst' = f env a1 a2 in
       if poly then
         if Constraint.is_empty cst' then cst
         else error (IncompatiblePolymorphism (env, a1, a2))
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 304e7e8470..948195797e 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -190,10 +190,10 @@ let warn_bytecode_compiler_failed =
          (fun () -> strbrk "Bytecode compiler failed, " ++
                       strbrk "falling back to standard conversion")
 
-let vm_conv_gen cv_pb env graph univs t1 t2 =
+let vm_conv_gen cv_pb env univs t1 t2 =
   if not (typing_flags env).Declarations.enable_VM then
     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-      TransparentState.full env graph univs t1 t2
+      TransparentState.full env univs t1 t2
   else
   try
     let v1 = val_of_constr env t1 in
@@ -202,7 +202,7 @@ let vm_conv_gen cv_pb env graph univs t1 t2 =
   with Not_found | Invalid_argument _ ->
     warn_bytecode_compiler_failed ();
     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-      TransparentState.full env graph univs t1 t2
+      TransparentState.full env univs t1 t2
 
 let vm_conv cv_pb env t1 t2 =
   let univs = Environ.universes env in
@@ -212,4 +212,4 @@ let vm_conv cv_pb env t1 t2 =
   in
   if not b then
     let state = (univs, checked_universes) in
-    let _ = vm_conv_gen cv_pb env univs state t1 t2 in ()
+    let _ = vm_conv_gen cv_pb env state t1 t2 in ()
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index bea62c8bef..db2f5c6209 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1163,10 +1163,10 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
       | None ->
         let x = EConstr.Unsafe.to_constr x in
         let y = EConstr.Unsafe.to_constr y in
-        let graph = Evd.universes sigma in
+        let env = Environ.set_universes (Evd.universes sigma) env in
         let sigma' =
           conv_fun pb ~l2r:false sigma ts
-            env graph (sigma, sigma_univ_state) x y in
+            env (sigma, sigma_univ_state) x y in
         Some sigma'
   with
   | Reduction.NotConvertible -> None