diff options
| -rw-r--r-- | theories/ZArith/Zsyntax.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index 12c7e017c..2b01710e9 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -172,6 +172,9 @@ Syntax constr -> [(MUTIND $i $n)] | mutconstruct_inside [ << (ZEXPR (MUTCONSTRUCT $c1 $c2 $c3)) >> ] -> [ (MUTCONSTRUCT $c1 $c2 $c3) ] + + | O_inside [ << (ZEXPR << O >>) >> ] -> [ "O" ] (* To shunt Arith printer *) + (* Added by JCF, 9/3/98; updated HH, 11/9/01 *) | implicit_head_inside [ << (ZEXPR (APPLISTEXPL ($LIST $c))) >> ] -> [ (APPLIST ($LIST $c)) ] |