diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-07 15:55:56 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-07 15:55:56 +0100 |
| commit | a15ae330fd156b74fcdfb4fc39b79013d3e398bf (patch) | |
| tree | df52975748b4e5737385589788482ad057d1e937 /kernel/cClosure.ml | |
| parent | 972c0e941a8acdd33053e2032ae0401b9aa4605d (diff) | |
| parent | e849572cd2b242b34fbec6c3eaa42e7d2e7cc550 (diff) | |
Merge PR #6685: Use whd-all on rigid-flex conversion.
Diffstat (limited to 'kernel/cClosure.ml')
| -rw-r--r-- | kernel/cClosure.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 7ed965b4c..219ea5b24 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 } |