diff options
Diffstat (limited to 'theories/Reals/Rsyntax.v')
| -rw-r--r-- | theories/Reals/Rsyntax.v | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v index 9022e4f7e..6cc0d71c4 100644 --- a/theories/Reals/Rsyntax.v +++ b/theories/Reals/Rsyntax.v @@ -59,9 +59,14 @@ with rexpr0 : constr := | expr_inv [ "/" rexpr0($c) ] -> [ (Rinv $c) ] | expr_meta [ meta($m) ] -> [ $m ] -with meta : ast := -| rimpl [ "?" ] -> [ (ISEVAR) ] -| rmeta [ "?" constr:numarg($n) ] -> [ (META $n) ] +with meta := +| rimpl [ "?" ] -> [ ? ] +| rmeta0 [ "?" "0" ] -> [ ?0 ] +| rmeta1 [ "?" "1" ] -> [ ?1 ] +| rmeta2 [ "?" "2" ] -> [ ?2 ] +| rmeta3 [ "?" "3" ] -> [ ?3 ] +| rmeta4 [ "?" "4" ] -> [ ?4 ] +| rmeta5 [ "?" "5" ] -> [ ?5 ] with rapplication : constr := apply [ rapplication($p) rexpr($c1) ] -> [ ($p $c1) ] |