From e849572cd2b242b34fbec6c3eaa42e7d2e7cc550 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 5 Feb 2018 13:56:22 +0100 Subject: Respect the transparent state of the current conversion on strong weak-head. This fixes the previous patch in rare corner-cases where unification code was relying on both kernel conversion and specific transparent state. --- kernel/reduction.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'kernel/reduction.ml') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index a152a5c5f..6104f56c6 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -483,6 +483,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = Conversion check to rigid terms eventually implies full weak-head reduction, so instead of repeatedly performing small-step unfoldings, we perform reduction with all flags on. *) + let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in let r1 = whd_stack (infos_with_reds infos all) def1 v1 in eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv | None -> @@ -499,6 +500,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (match unfold_reference infos fl2 with | Some def2 -> (** Symmetrical case of above. *) + let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in let r2 = whd_stack (infos_with_reds infos all) def2 v2 in eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv | None -> -- cgit v1.2.3