diff options
| author | Jason Gross | 2019-03-31 15:35:21 -0400 |
|---|---|---|
| committer | Jason Gross | 2019-04-01 11:41:58 -0400 |
| commit | 73c924d3d4bcc22a179cb974603f9072599ebb77 (patch) | |
| tree | 162be6d2b1f3093e8470e58b19b3eb9151cab534 | |
| parent | 63f454f772164dc293390f07c5ec674ab21724a9 (diff) | |
Update numeral notation printing doc
Fixes #9844
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 8 | ||||
| -rw-r--r-- | interp/notation.ml | 8 |
2 files changed, 15 insertions, 1 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index e5eb7eb4f5..1e201953b3 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1473,6 +1473,10 @@ Numeral notations :n:`@ident__2` to the number will be fully reduced, and universes of the resulting term will be refreshed. + Note that only fully-reduced ground terms (terms containing only + function application, constructors, inductive type families, and + primitive integers) will be considered for printing. + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). When a literal larger than :token:`num` is parsed, a warning @@ -1618,6 +1622,10 @@ String notations :n:`@ident__2` to the string will be fully reduced, and universes of the resulting term will be refreshed. + Note that only fully-reduced ground terms (terms containing only + function application, constructors, inductive type families, and + primitive integers) will be considered for printing. + .. exn:: Cannot interpret this string as a value of type @type The string notation registered for :token:`type` does not support diff --git a/interp/notation.ml b/interp/notation.ml index b5e91b17e6..2765661749 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -626,7 +626,13 @@ exception NotAValidPrimToken (** The uninterp function below work at the level of [glob_constr] which is too low for us here. So here's a crude conversion back - to [constr] for the subset that concerns us. *) + to [constr] for the subset that concerns us. + + Note that if you update [constr_of_glob], you should update the + corresponding numeral notation *and* string notation doc in + doc/sphinx/user-extensions/syntax-extensions.rst that describes + what it means for a term to be ground / to be able to be + considered for parsing. *) let rec constr_of_glob env sigma g = match DAst.get g with | Glob_term.GRef (ConstructRef c, _) -> |