From 64e7be2e88f01ad65928e4b2b537e60c2c4e9260 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 27 Jun 2016 23:41:19 +0200
Subject: Properly handling the only printing flag when parsing rules already
 exist.

---
 interp/notation.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation.mli')

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
 
-- 
cgit v1.2.3