diff options
| author | Hugo Herbelin | 2020-02-10 18:54:55 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-16 21:44:43 +0100 |
| commit | 6eb4dbf6ba77ae7e9087832ea1e27426b515a8e8 (patch) | |
| tree | 27a68854587a73a4ec91e283f6e1e0d681810bb7 /vernac/egramcoq.ml | |
| parent | 376e92f87a73afb9d848cea9895d75c932b2b25a (diff) | |
Custom entries: accept that no level is mentioned for a subentry.
If it is for an internal non-terminal then:
- if for a subentry different from constr, it refers to the head of
the subentry
- if in constr, it is 200 by convention
If it is on the border of a rule, then:
- if it is in a subentry different from the entry it lives, it refers
to the head of the subentry (or 200 by convention if in constr)
- if it is in the same entry, the rule for associativity tells if a
SELF, a NEXT, or (if on the right) a LEVEL
Diffstat (limited to 'vernac/egramcoq.ml')
| -rw-r--r-- | vernac/egramcoq.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |