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 -
 doc/tools/docgram/orderedGrammar | 1 -
 2 files changed, 2 deletions(-)

(limited to 'doc/tools')

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