aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Prelude.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init/Prelude.v')
-rwxr-xr-xtheories/Init/Prelude.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 5f647f373..6cdc8d0b4 100755
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -15,4 +15,5 @@ Require Export LogicSyntax.
Require Export Specif.
Require Export SpecifSyntax.
Require Export Peano.
+Require Export PeanoSyntax.
Require Export Wf.