diff options
| -rw-r--r-- | contrib/ring/Quote.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v index 609328d1a6..abde178e11 100644 --- a/contrib/ring/Quote.v +++ b/contrib/ring/Quote.v @@ -79,7 +79,7 @@ Implicit Arguments Off. Declare ML Module "quote". -Grammar tactic simple_tactic := +Grammar tactic simple_tactic : Ast := quote [ "Quote" identarg($f) ] -> [(Quote $f)] | quote_lc [ "Quote" identarg($f) "[" ne_identarg_list($lc) "]"] -> - [(Quote $f ($LIST $lc))]. + [ (Quote $f ($LIST $lc)) ]. |