diff options
| author | coqbot-app[bot] | 2021-04-12 17:50:05 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-12 17:50:05 +0000 |
| commit | b78e6cfcb412d1c4e5902fb895c5ecaa0cb177ac (patch) | |
| tree | fc6dc321767aa78bb57660bcac07018147b540c0 /doc/tools | |
| parent | bba57138fcb0badf307fb00b97d73b4933e3022b (diff) | |
| parent | 09fb4762de8b2dc256a43d6a931d5a479b98cd26 (diff) | |
Merge PR #14107: Gitignore update for doc_grammar and omega clean-up.
Reviewed-by: jfehrle
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 1 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 1 |
2 files changed, 0 insertions, 2 deletions
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index ab1a9d4c75..0c8980b1bd 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1778,7 +1778,6 @@ simple_tactic: [ | "zify_iter_let" tactic (* micromega plugin *) | "zify_elim_let" (* micromega plugin *) | "nsatz_compute" constr (* nsatz plugin *) -| "omega" (* omega plugin *) | "protect_fv" string "in" ident (* ring plugin *) | "protect_fv" string (* ring plugin *) | "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr (* ring plugin *) diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 5b19b7fc55..40bb980e90 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1856,7 +1856,6 @@ simple_tactic: [ | "zify_iter_let" ltac_expr (* micromega plugin *) | "zify_elim_let" (* micromega plugin *) | "nsatz_compute" one_term (* nsatz plugin *) -| "omega" (* omega plugin *) | "protect_fv" string OPT ( "in" ident ) | "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) | "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) |