diff options
| author | Jim Fehrle | 2020-10-12 10:37:09 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-10-12 10:37:09 -0700 |
| commit | bdc5db891aa2a060387da758d8910a82cea21da1 (patch) | |
| tree | 8122c3a46ee68b7b5f0f3c263d8516a40e08347c /doc/tools/docgram/fullGrammar | |
| parent | 03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (diff) | |
Add missing ";" in record grammar
Diffstat (limited to 'doc/tools/docgram/fullGrammar')
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 067050b4f5..73641976e3 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1740,11 +1740,11 @@ simple_tactic: [ | "zify_elim_let" (* micromega plugin *) | "nsatz_compute" constr (* nsatz plugin *) | "omega" (* omega plugin *) -| "rtauto" | "protect_fv" string "in" ident (* ring plugin *) | "protect_fv" string (* ring plugin *) | "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* ring plugin *) | "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr (* ring plugin *) +| "rtauto" ] mlname: [ |