diff options
| -rw-r--r-- | kernel/mod_typing.ml | 10 | ||||
| -rw-r--r-- | kernel/nativeconv.ml | 6 | ||||
| -rw-r--r-- | kernel/reduction.ml | 20 | ||||
| -rw-r--r-- | kernel/reduction.mli | 4 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 2 | ||||
| -rw-r--r-- | kernel/vconv.ml | 8 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 4 |
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 |