diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/ExtractBase.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 14ce4119..feab7706 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -240,7 +240,9 @@ type formatter = { - loop identifier, if this is for a loop *) opaque_pre : unit -> string; - (** The prefix to use for opaque definitions. + (** TODO: obsolete, remove. + + The prefix to use for opaque definitions. We need this because for some backends like Lean and Coq, we group opaque definitions in module signatures, meaning that using those |