diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/tools/docgram/doc_grammar.ml | 3 |
1 files changed, 1 insertions, 2 deletions
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"; ] |