diff options
Diffstat (limited to 'theories/Init/Prelude.v')
| -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 *) |