diff options
| author | coqbot-app[bot] | 2021-04-21 14:58:51 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-21 14:58:51 +0000 |
| commit | f9996cdaf0b6aee12c5b71432b1edb90dffb569a (patch) | |
| tree | 99bacd74ac72db0aed31f18280b08be3db794db2 /doc/tools/docgram/fullGrammar | |
| parent | 3645c06030ed1266fd4160ec7211b4447731bf13 (diff) | |
| parent | eeb142f3c69d2467fbadd7dd1470ac1606b2e5bf (diff) | |
Merge PR #13911: Remove the :> type cast?
Reviewed-by: mattam82
Ack-by: Zimmi48
Diffstat (limited to 'doc/tools/docgram/fullGrammar')
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 0c8980b1bd..fe166524bf 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1,6 +1,15 @@ (* Coq grammar generated from .mlg files. Do not edit by hand. Not compiled into Coq *) DOC_GRAMMAR +vernac_toplevel: [ +| "Drop" "." +| "Quit" "." +| "BackTo" natural "." +| test_show_goal "Show" "Goal" natural "at" natural "." +| "Show" "Proof" "Diffs" OPT "removed" "." +| Pvernac.Vernac_.main_entry +] + Constr.ident: [ | Prim.ident ] @@ -75,7 +84,6 @@ term100: [ | term99 "<:" term200 | term99 "<<:" term200 | term99 ":" term200 -| term99 ":>" | term99 ] @@ -478,15 +486,6 @@ strategy_level: [ | "transparent" ] -vernac_toplevel: [ -| "Drop" "." -| "Quit" "." -| "BackTo" natural "." -| test_show_goal "Show" "Goal" natural "at" natural "." -| "Show" "Proof" "Diffs" OPT "removed" "." -| Pvernac.Vernac_.main_entry -] - opt_hintbases: [ | | ":" LIST1 IDENT |