aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/mod_typing.ml10
-rw-r--r--kernel/nativeconv.ml4
-rw-r--r--kernel/reduction.ml42
-rw-r--r--kernel/reduction.mli6
-rw-r--r--kernel/subtyping.ml2
-rw-r--r--kernel/typeops.mli2
-rw-r--r--kernel/vconv.ml4
-rw-r--r--plugins/ssrmatching/ssrmatching.ml3
-rw-r--r--pretyping/reductionops.ml10
-rw-r--r--pretyping/typing.ml3
10 files changed, 41 insertions, 45 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 01e9550ec5..fc6afb79d4 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -176,7 +176,7 @@ let native_conv cv_pb sigma env t1 t2 =
else Constr.eq_constr_univs univs t1 t2
in
if not b then
- let univs = (univs, checked_universes) in
+ 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 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 7c6b869b4a..96bf370342 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -189,7 +189,7 @@ type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
(* functions of this type can be called from outside the kernel *)
type 'a extended_conversion_function =
?l2r:bool -> ?reds:TransparentState.t -> env ->
- ?evars:((existential->constr option) * UGraph.t) ->
+ ?evars:(existential->constr option) ->
'a -> 'a -> unit
exception NotConvertible
@@ -210,9 +210,6 @@ type conv_pb =
let is_cumul = function CUMUL -> true | CONV -> false
type 'a universe_compare = {
- (* used in reduction *)
- compare_graph : 'a -> UGraph.t;
-
(* Might raise NotConvertible *)
compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
@@ -224,7 +221,7 @@ type 'a universe_state = 'a * 'a universe_compare
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)
@@ -765,9 +762,8 @@ and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with
convert_list l2r infos lft1 lft2 v1 v2 cuniv
| _, _ -> raise NotConvertible
-let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
+let clos_gen_conv trans cv_pb l2r evars env graph univs t1 t2 =
let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
- let graph = (snd univs).compare_graph (fst univs) in
let infos = create_clos_infos ~univs:graph ~evars reds env in
let infos = {
cnv_inf = infos;
@@ -815,8 +811,7 @@ let check_inductive_instances cv_pb variance u1 u2 univs =
else raise NotConvertible
let checked_universes =
- { compare_graph = (fun x -> x);
- compare_sorts = checked_sort_cmp_universes;
+ { compare_sorts = checked_sort_cmp_universes;
compare_instances = check_convert_instances;
compare_cumul_instances = check_inductive_instances; }
@@ -878,8 +873,7 @@ let infer_inductive_instances cv_pb variance u1 u2 (univs,csts') =
(univs, Univ.Constraint.union csts csts')
let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
- { compare_graph = (fun (x,_) -> x);
- compare_sorts = infer_cmp_universes;
+ { compare_sorts = infer_cmp_universes;
compare_instances = infer_convert_instances;
compare_cumul_instances = infer_inductive_instances; }
@@ -890,12 +884,12 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 =
in
if b then ()
else
- let _ = clos_gen_conv reds cv_pb l2r evars env (univs, checked_universes) t1 t2 in
+ let _ = clos_gen_conv reds cv_pb l2r evars env univs (univs, checked_universes) t1 t2 in
()
(* Profiling *)
-let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None), universes env) =
- let evars, univs = evars in
+let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None)) =
+ let univs = Environ.universes env in
if Flags.profile then
let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in
CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs
@@ -906,35 +900,37 @@ let conv = gen_conv CONV
let conv_leq = gen_conv CUMUL
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 univs t1 t2
+ 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
in
if b then cstrs
else
- let univs = ((univs, Univ.Constraint.empty), inferred_universes) in
- let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs t1 t2 in
+ let state = ((univs, Univ.Constraint.empty), inferred_universes) in
+ let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs state t1 t2 in
cstrs
(* Profiling *)
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 4ae3838691..7d32596f74 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -31,14 +31,12 @@ exception NotConvertible
type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
type 'a extended_conversion_function =
?l2r:bool -> ?reds:TransparentState.t -> env ->
- ?evars:((existential->constr option) * UGraph.t) ->
+ ?evars:(existential->constr option) ->
'a -> 'a -> unit
type conv_pb = CONV | CUMUL
type 'a universe_compare = {
- compare_graph : 'a -> UGraph.t; (* used for case inversion in reduction *)
-
(* Might raise NotConvertible *)
compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
@@ -50,7 +48,7 @@ type 'a universe_state = 'a * 'a universe_compare
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/typeops.mli b/kernel/typeops.mli
index 87a5666fcc..d381e55dd6 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -111,7 +111,7 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
(** {6 Miscellaneous. } *)
(** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) ->
+val check_hyps_inclusion : env -> ?evars:(existential->constr option) ->
GlobRef.t -> Constr.named_context -> unit
(** Types for primitives *)
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index cc2c2c0b4b..948195797e 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -211,5 +211,5 @@ let vm_conv cv_pb env t1 t2 =
else Constr.eq_constr_univs univs t1 t2
in
if not b then
- let univs = (univs, checked_universes) in
- let _ = vm_conv_gen cv_pb env univs t1 t2 in ()
+ let state = (univs, checked_universes) in
+ let _ = vm_conv_gen cv_pb env state t1 t2 in ()
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 5dedae6388..cdd15acb0d 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -204,7 +204,8 @@ exception NoProgress
(* comparison can be much faster than the HO one. *)
let unif_EQ env sigma p c =
- let evars = existential_opt_value0 sigma, Evd.universes sigma in
+ let env = Environ.set_universes (Evd.universes sigma) env in
+ let evars = existential_opt_value0 sigma in
try let _ = Reduction.conv env p ~evars c in true with _ -> false
let unif_EQ_args env sigma pa a =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 08a6db5639..3352bfce38 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1094,7 +1094,8 @@ let f_conv_leq ?l2r ?reds env ?evars x y =
let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y =
try
let evars ev = safe_evar_value sigma ev in
- let _ = f ~reds env ~evars:(evars, Evd.universes sigma) x y in
+ let env = Environ.set_universes (Evd.universes sigma) env in
+ let _ = f ~reds env ~evars x y in
true
with Reduction.NotConvertible -> false
| e ->
@@ -1112,7 +1113,8 @@ let check_conv ?(pb=Reduction.CUMUL) ?(ts=TransparentState.full) env sigma x y =
| Reduction.CONV -> f_conv
| Reduction.CUMUL -> f_conv_leq
in
- try f ~reds:ts env ~evars:(safe_evar_value sigma, Evd.universes sigma) x y; true
+ let env = Environ.set_universes (Evd.universes sigma) env in
+ try f ~reds:ts env ~evars:(safe_evar_value sigma) x y; true
with Reduction.NotConvertible -> false
| Univ.UniverseInconsistency _ -> false
| e ->
@@ -1138,8 +1140,7 @@ let sigma_check_inductive_instances cv_pb variance u1 u2 sigma =
let sigma_univ_state =
let open Reduction in
- { compare_graph = Evd.universes;
- compare_sorts = sigma_compare_sorts;
+ { compare_sorts = sigma_compare_sorts;
compare_instances = sigma_compare_instances;
compare_cumul_instances = sigma_check_inductive_instances; }
@@ -1164,6 +1165,7 @@ 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 env = Environ.set_universes (Evd.universes sigma) env in
let sigma' =
conv_fun pb ~l2r:false sigma ts
env (sigma, sigma_univ_state) x y in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 40d3faa98c..aeb3873de7 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -297,7 +297,8 @@ let judge_of_letin env name defj typj j =
uj_type = subst1 defj.uj_val j.uj_type }
let check_hyps_inclusion env sigma x hyps =
- let evars = Evarutil.safe_evar_value sigma, Evd.universes sigma in
+ let env = Environ.set_universes (Evd.universes sigma) env in
+ let evars = Evarutil.safe_evar_value sigma in
Typeops.check_hyps_inclusion env ~evars x hyps
let type_of_constant env sigma (c,u) =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:44:28 +0000