From b6214bd4d5d3003e9b60411a717e84277feead24 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:27:00 +0200
Subject: [string notation] Handle parameterized inductives and non inductives

---
 plugins/syntax/string_notation.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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

diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli
index 0d99f98d26..f3c7c969c6 100644
--- a/plugins/syntax/string_notation.mli
+++ b/plugins/syntax/string_notation.mli
@@ -14,5 +14,7 @@ open Vernacexpr
 (** * String notation *)
 
 val vernac_string_notation : locality_flag ->
-                             qualid -> qualid -> qualid ->
+                             qualid ->
+                             qualid -> qualid ->
+                             Number.number_string_via option ->
                              Notation_term.scope_name -> unit
-- 
cgit v1.2.3