diff options
| -rw-r--r-- | parsing/pcoq.ml4 | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 9c206565e..6472dbaf5 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -482,7 +482,11 @@ let dynconstr = Gram.Entry.create "Constr.dynconstr" let dyncasespattern = Gram.Entry.create "Constr.dyncasespattern" GEXTEND Gram - dynconstr: [ [ a = Constr.constr -> ConstrNode a ] ]; + dynconstr: + [ [ a = Constr.constr -> ConstrNode a + (* For compatibility *) + | "<<"; a = Constr.constr; ">>" -> ConstrNode a ] ] + ; dyncasespattern: [ [ a = Constr.pattern -> CasesPatternNode a ] ]; END |