diff options
| author | Pierre Roux | 2020-09-03 13:27:00 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-11-05 00:20:51 +0100 |
| commit | b6214bd4d5d3003e9b60411a717e84277feead24 (patch) | |
| tree | cd0a04bbf1b9e43d21ec5944c4458d74797c5b09 /plugins/syntax/string_notation.mli | |
| parent | 3b766fd8859b692e3e93cf83bf87d393e32c572e (diff) | |
[string notation] Handle parameterized inductives and non inductives
Diffstat (limited to 'plugins/syntax/string_notation.mli')
| -rw-r--r-- | plugins/syntax/string_notation.mli | 4 |
1 files changed, 3 insertions, 1 deletions
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 |