diff options
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 8 | ||||
| -rw-r--r-- | vernac/egramcoq.ml | 3 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 9 |
3 files changed, 11 insertions, 9 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index dbe714c388..a8d5ac610f 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -798,7 +798,13 @@ associated to the custom entry ``expr``. The level can be omitted, as in Notation "[ e ]" := e (e custom expr). -in which case Coq tries to infer it. +in which case Coq infer it. If the sub-expression is at a border of +the notation (as e.g. ``x`` and ``y`` in ``x + y``), the level is +determined by the associativity. If the sub-expression is not at the +border of the notation (as e.g. ``e`` in ``"[ e ]``), the level is +inferred to be the highest level used for the entry. In particular, +this level depends on the highest level existing in the entry at the +time of use of the notation. In the absence of an explicit entry for parsing or printing a sub-expression of a notation in a custom entry, the default is to diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index bf49fb4df5..9f41287bce 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -213,7 +213,8 @@ let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in mat (* If a default level in a different grammar, the entry name is ok *) | (DefaultLevel,InternalProd) -> if Notation.notation_entry_eq custom InConstrEntry then NumLevel 200 else DefaultLevel - | (DefaultLevel,BorderProd _) when not (Notation.notation_entry_eq custom custom') -> DefaultLevel + | (DefaultLevel,BorderProd _) when not (Notation.notation_entry_eq custom custom') -> + if Notation.notation_entry_eq custom InConstrEntry then NumLevel 200 else DefaultLevel (* Associativity is None means force the level *) | (NumLevel n,BorderProd (_,None)) -> NumLevel n | (DefaultLevel,BorderProd (_,None)) -> assert false diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 1e46d35ed7..7794b0a37a 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -978,17 +978,12 @@ let is_only_printing mods = let set_entry_type from n etyps (x,typ) = let make_lev n s = match typ with | BorderProd _ -> NumLevel n - | InternalProd -> - if s = InConstrEntry then NumLevel 200 else - user_err (strbrk "level of inner subentry " ++ quote (pr_notation_entry s) ++ - str " cannot be inferred. It must be given explicitly.") in + | InternalProd -> DefaultLevel in let typ = try match List.assoc x etyps, typ with | ETConstr (s,bko,DefaultLevel), _ -> if notation_entry_eq from s then ETConstr (s,bko,(make_lev n s,typ)) - else if s = InConstrEntry then ETConstr (s,bko,(make_lev 200 s,typ)) else - user_err (strbrk "level of subentry " ++ quote (pr_notation_entry s) ++ - str " cannot be inferred. It must be given explicitly.") + else ETConstr (s,bko,(DefaultLevel,typ)) | ETConstr (s,bko,n), BorderProd (left,_) -> ETConstr (s,bko,(n,BorderProd (left,None))) | ETConstr (s,bko,n), InternalProd -> |