diff options
| author | Maxime Dénès | 2020-06-16 17:09:40 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-07-03 13:13:02 +0200 |
| commit | 53e19f76624b7a18792af799e970e9478f8e90a9 (patch) | |
| tree | b852fd1e116ff72748210a11bc95298453ac2e4d /parsing/g_constr.mlg | |
| parent | 33581635d3ad525e1d5c2fb2587be345a7e77009 (diff) | |
Fix #11121: Simultaneous definition of term and notation in custom grammar
Diffstat (limited to 'parsing/g_constr.mlg')
| -rw-r--r-- | parsing/g_constr.mlg | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index c19dd00b38..429e740403 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -165,11 +165,11 @@ GRAMMAR EXTEND Gram collapse -(3) into the numeral -3. *) (match c.CAst.v with | CPrim (Numeral (NumTok.SPlus,n)) -> - CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"( _ )"),([c],[],[],[])) + CAst.make ~loc @@ CNotation(None,(InConstrEntry,"( _ )"),([c],[],[],[])) | _ -> c) } | "{|"; c = record_declaration; bar_cbrace -> { c } | "{"; c = binder_constr ; "}" -> - { CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) } + { CAst.make ~loc @@ CNotation(None,(InConstrEntry,"{ _ }"),([c],[],[],[])) } | "`{"; c = operconstr LEVEL "200"; "}" -> { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) } | "`("; c = operconstr LEVEL "200"; ")" -> @@ -346,7 +346,7 @@ GRAMMAR EXTEND Gram collapse -(3) into the numeral -3. *) match p.CAst.v with | CPatPrim (Numeral (NumTok.SPlus,n)) -> - CAst.make ~loc @@ CPatNotation(None,(InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) + CAst.make ~loc @@ CPatNotation(None,(InConstrEntry,"( _ )"),([p],[]),[]) | _ -> p } | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" -> { CAst.make ~loc @@ CPatOr (p::pl) } |