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.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'kernel/cClosure.mli') diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 119b70e30..41db0af75 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -61,6 +61,9 @@ module type RedFlagsSig = sig (** Adds a reduction kind to a set *) val red_add_transparent : reds -> transparent_state -> reds + (** Retrieve the transparent state of the reduction flags *) + val red_transparent : reds -> transparent_state + (** Build a reduction set from scratch = iter [red_add] on [no_red] *) val mkflags : red_kind list -> reds -- cgit v1.2.3