diff options
| author | Théo Zimmermann | 2021-04-12 16:38:50 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2021-04-12 16:38:55 +0200 |
| commit | 09fb4762de8b2dc256a43d6a931d5a479b98cd26 (patch) | |
| tree | b4db15f9645b02dbd76b785e6547a96841c0820e /doc/tools/docgram/orderedGrammar | |
| parent | 906b88c665d12f31aa9cd584fc2c7c66edef434f (diff) | |
Remove omega from doc_grammar files.
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 1 |
1 files changed, 0 insertions, 1 deletions
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 *) |