From cf868740c3d18ee9ce9a6b38dd617784625a3cae Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 9 Jan 2019 15:32:52 -0800
Subject: Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg
 files and inserting it into the .rst files

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

(limited to '.gitignore')

diff --git a/.gitignore b/.gitignore
index 5339a0c44d..93b874eae3 100644
--- a/.gitignore
+++ b/.gitignore
@@ -110,6 +110,9 @@ doc/stdlib/FullLibrary.coqdoc.tex
 doc/stdlib/html/
 doc/stdlib/index-body.html
 doc/stdlib/index-list.html
+doc/tools/docgram/productionlistGrammar
+doc/tools/docgram/editedGrammar
+doc/tools/docgram/prodnGrammar
 doc/tutorial/Tutorial.v.out
 doc/RecTutorial/RecTutorial.html
 doc/RecTutorial/RecTutorial.ps
-- 
cgit v1.2.3