From 4476f64dc87fb86738fc4c9f939113b70843c035 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 18 Sep 2020 14:15:18 +0200
Subject: {new,setoid_}ring -> ring

I believe this renaming makes it easier for new contributors to discover
the code of `ring`.
---
 doc/tools/docgram/dune | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/tools')

diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune
index ba07e6df0d..2a7b283f55 100644
--- a/doc/tools/docgram/dune
+++ b/doc/tools/docgram/dune
@@ -24,7 +24,7 @@
    (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/setoid_ring/*.mlg)
+   (glob_files %{project_root}/plugins/ring/*.mlg)
    (glob_files %{project_root}/plugins/syntax/*.mlg)
    (glob_files %{project_root}/user-contrib/Ltac2/*.mlg)
    ; Sphinx files
-- 
cgit v1.2.3