diff options
| author | Pierre-Marie Pédrot | 2016-06-28 01:20:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-28 01:20:11 +0200 |
| commit | f57b6e3478f3a64a1f8d669ff256d9506ba67688 (patch) | |
| tree | c3c266d03e5c680bfee31011d57a74634fde0dfc /interp/notation.mli | |
| parent | 9f9c1dc37ca3ffe30417c8f7b63d62ad5b63e51b (diff) | |
| parent | ee0d4870fb982877be7cf07c75e3d039b82ddfc0 (diff) | |
Finalizing the only printing feature.
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index a85dc50f2f..b47e1975e3 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -109,7 +109,7 @@ type interp_rule = | SynDefRule of kernel_name val declare_notation_interpretation : notation -> scope_name option -> - interpretation -> notation_location -> unit + interpretation -> notation_location -> onlyprint:bool -> unit val declare_uninterpretation : interp_rule -> interpretation -> unit |