From 3b766fd8859b692e3e93cf83bf87d393e32c572e Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:26:00 +0200
Subject: Merge numeral and string notation plugins

---
 doc/tools/docgram/doc_grammar.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index b7f1e18d2b..92bcd51528 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -538,12 +538,11 @@ let autoloaded_mlgs = [ (* in the order they are loaded by Coq *)
  "plugins/ltac/g_eqdecide.mlg";
  "plugins/ltac/g_tactic.mlg";
  "plugins/ltac/g_ltac.mlg";
- "plugins/syntax/g_string.mlg";
  "plugins/btauto/g_btauto.mlg";
  "plugins/rtauto/g_rtauto.mlg";
  "plugins/cc/g_congruence.mlg";
  "plugins/firstorder/g_ground.mlg";
- "plugins/syntax/g_numeral.mlg";
+ "plugins/syntax/g_number_string.mlg";
 ]
 
 
-- 
cgit v1.2.3