From 0520decfdc94d52a2f8658b9cf6a730e6d333f8f Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:23:00 +0200
Subject: [numeral notation] Handle implicit arguments

---
 plugins/syntax/numeral.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/syntax/numeral.mli')

diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index 1f6896d549..5a13d1068b 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -14,7 +14,7 @@ open Notation
 
 (** * Number notation *)
 
-type number_string_via = qualid * (qualid * qualid) list
+type number_string_via = qualid * (bool * qualid * qualid) list
 type number_option =
   | After of numnot_option
   | Via of number_string_via
-- 
cgit v1.2.3