diff options
Diffstat (limited to 'kernel/conv_oracle.ml')
| -rw-r--r-- | kernel/conv_oracle.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index a4eab42d0..7da2a7faa 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -19,6 +19,9 @@ open Names type level = Expand | Level of int | Opaque let default = Level 0 let transparent = default +let is_transparent = function +| Level 0 -> true +| _ -> false type oracle = level Idmap.t * level Cmap.t |