From 09fb4762de8b2dc256a43d6a931d5a479b98cd26 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 12 Apr 2021 16:38:50 +0200
Subject: Remove omega from doc_grammar files.

---
 doc/tools/docgram/fullGrammar | 1 -
 1 file changed, 1 deletion(-)

(limited to 'doc/tools/docgram/fullGrammar')

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 *)
-- 
cgit v1.2.3