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/cClosure.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'kernel/cClosure.ml') diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index b1181157e..4fd274ae1 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -91,6 +91,7 @@ module type RedFlagsSig = sig val red_add : reds -> red_kind -> reds val red_sub : reds -> red_kind -> reds val red_add_transparent : reds -> transparent_state -> reds + val red_transparent : reds -> transparent_state val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool val red_projection : reds -> projection -> bool @@ -164,6 +165,8 @@ module RedFlags = (struct let (l1,l2) = red.r_const in { red with r_const = Id.Pred.remove id l1, l2 } + let red_transparent red = red.r_const + let red_add_transparent red tr = { red with r_const = tr } -- cgit v1.2.3