diff options
| author | Pierre Letouzey | 2018-04-06 16:37:47 +0200 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:53 -0400 |
| commit | 93119295d0dd81669b46f52032c1bfe8f36afca0 (patch) | |
| tree | 1da3e4a03e3893c30d72c0612660974b3ea2459d | |
| parent | 3c2331a4a9d8c5d5f27c90185c616fe3400d4f1f (diff) | |
Prelude : update the comment about ML plugins loaded by Init
| -rw-r--r-- | theories/Init/Prelude.v | 7 |
1 files 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 *) |