diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-02 14:10:13 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-02 14:41:23 +0100 |
| commit | c9839e30e1b46e70c85533d95e4f4cc2ae826c66 (patch) | |
| tree | c2b64c78b51aa85f66020d8c89e4a59888fc380f /checker/closure.mli | |
| parent | 338bac67b6c1111229d90c45875653171bbed4b3 (diff) | |
checker: remove unused per-constant reduction flags.
Diffstat (limited to 'checker/closure.mli')
| -rw-r--r-- | checker/closure.mli | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/checker/closure.mli b/checker/closure.mli index ce8c64e30..aace21f2b 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -24,14 +24,6 @@ val with_stats: 'a Lazy.t -> 'a Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of a LetIn expression is Letin reduction *) -type transparent_state = Id.Pred.t * Cpred.t - -val all_opaque : transparent_state -val all_transparent : transparent_state - -val is_transparent_variable : transparent_state -> variable -> bool -val is_transparent_constant : transparent_state -> Constant.t -> bool - (* Sets of reduction kinds. *) module type RedFlagsSig = sig type reds @@ -42,8 +34,6 @@ module type RedFlagsSig = sig val fDELTA : red_kind val fIOTA : red_kind val fZETA : red_kind - val fCONST : Constant.t -> red_kind - val fVAR : Id.t -> red_kind (* No reduction at all *) val no_red : reds |