summaryrefslogtreecommitdiff
path: root/plugins/extraction/ExtrOcamlBasic.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/ExtrOcamlBasic.v')
-rw-r--r--plugins/extraction/ExtrOcamlBasic.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v
index c9556972..882bcae9 100644
--- a/plugins/extraction/ExtrOcamlBasic.v
+++ b/plugins/extraction/ExtrOcamlBasic.v
@@ -8,6 +8,8 @@
(** Extraction to Ocaml : use of basic Ocaml types *)
+Scheme Equality for nat.
+
Extract Inductive bool => bool [ true false ].
Extract Inductive option => option [ Some None ].
Extract Inductive unit => unit [ "()" ].