diff options
| author | Pierre-Marie Pédrot | 2020-05-11 12:18:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-11 12:18:40 +0200 |
| commit | 0abac9befe6f165dd7829430a229192e6cb18453 (patch) | |
| tree | 744c8d39701f3226c4fc3bdbaafc10bada0b2de7 /kernel/conv_oracle.ml | |
| parent | aab47903fb2d3e0085b03d5ade94f4ae644cd76c (diff) | |
| parent | 6e4ebb2dbaa2cb9eb70ce205386bee08c80aaa00 (diff) | |
Merge PR #12129: Add a `with_strategy` tactic
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: herbelin
Ack-by: ppedrot
Diffstat (limited to 'kernel/conv_oracle.ml')
| -rw-r--r-- | kernel/conv_oracle.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 9b87c194c5..3ee1d2fb1f 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -19,6 +19,12 @@ open Names * The default value is [Level 100]. *) type level = Expand | Level of int | Opaque +let pr_level = function + | Expand -> Pp.str "expand" + | Level 0 -> Pp.str "transparent" + | Level n -> Pp.int n + | Opaque -> Pp.str "opaque" + let default = Level 0 let is_default = function | Level 0 -> true |