From 53aa272821c2cd94e4b05382fa33449e851c7a90 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 13 Nov 2020 09:20:21 +0100
Subject: Fix dune rules for @check-gram following recent changes.

---
 doc/tools/docgram/dune | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune
index 2a7b283f55..1c07d00d4f 100644
--- a/doc/tools/docgram/dune
+++ b/doc/tools/docgram/dune
@@ -12,7 +12,6 @@
    (glob_files %{project_root}/parsing/*.mlg)
    (glob_files %{project_root}/toplevel/*.mlg)
    (glob_files %{project_root}/vernac/*.mlg)
-   ; All plugins except SSReflect for now (mimicking what is done in Makefile.doc)
    (glob_files %{project_root}/plugins/btauto/*.mlg)
    (glob_files %{project_root}/plugins/cc/*.mlg)
    (glob_files %{project_root}/plugins/derive/*.mlg)
@@ -23,8 +22,11 @@
    (glob_files %{project_root}/plugins/micromega/*.mlg)
    (glob_files %{project_root}/plugins/nsatz/*.mlg)
    (glob_files %{project_root}/plugins/omega/*.mlg)
-   (glob_files %{project_root}/plugins/rtauto/*.mlg)
    (glob_files %{project_root}/plugins/ring/*.mlg)
+   (glob_files %{project_root}/plugins/rtauto/*.mlg)
+   (glob_files %{project_root}/plugins/ssr/*.mlg)
+   (glob_files %{project_root}/plugins/ssrmatching/*.mlg)
+   (glob_files %{project_root}/plugins/ssrsearch/*.mlg)
    (glob_files %{project_root}/plugins/syntax/*.mlg)
    (glob_files %{project_root}/user-contrib/Ltac2/*.mlg)
    ; Sphinx files
-- 
cgit v1.2.3