diff options
Diffstat (limited to 'theories/Init/Prelude.v')
| -rw-r--r-- | theories/Init/Prelude.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 84de55e24..685c72470 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -15,7 +15,8 @@ Require Export Specif. Require Export Peano. Require Export Coq.Init.Wf. Require Export Coq.Init.Tactics. -(* Initially available plugins *) +(* Initially available plugins + (+ nat_syntax_plugin loaded in Datatypes) *) Declare ML Module "extraction_plugin". Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". |