From 93119295d0dd81669b46f52032c1bfe8f36afca0 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Fri, 6 Apr 2018 16:37:47 +0200
Subject: Prelude : update the comment about ML plugins loaded by Init

---
 theories/Init/Prelude.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 802f18c0f2..390ff5e240 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -19,8 +19,11 @@ Require Export Peano.
 Require Export Coq.Init.Wf.
 Require Export Coq.Init.Tactics.
 Require Export Coq.Init.Tauto.
-(* Initially available plugins
-   (+ nat_syntax_plugin loaded in Datatypes) *)
+(* Some initially available plugins. See also:
+   - ltac_plugin (in Notations)
+   - nat_syntax_plugin (in Datatypes)
+   - tauto_plugin (in Tauto).
+*)
 Declare ML Module "cc_plugin".
 Declare ML Module "ground_plugin".
 (* Default substrings not considered by queries like SearchAbout *)
-- 
cgit v1.2.3