From 906b88c665d12f31aa9cd584fc2c7c66edef434f Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 12 Apr 2021 16:38:24 +0200
Subject: Gitignore update for doc_grammar.

---
 .gitignore | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.gitignore b/.gitignore
index bf7430cc2e..1abead3c67 100644
--- a/.gitignore
+++ b/.gitignore
@@ -115,6 +115,9 @@ doc/stdlib/index-body.html
 doc/stdlib/index-list.html
 doc/tools/docgram/editedGrammar
 doc/tools/docgram/prodnGrammar
+doc/tools/docgram/prodnCommands
+doc/tools/docgram/prodnTactics
+doc/tools/docgram/updated_rsts
 doc/unreleased.rst
 
 # .mll files
-- 
cgit v1.2.3


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(-)

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