summaryrefslogtreecommitdiff
path: root/plugins/extraction/ExtrOcamlString.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/ExtrOcamlString.v')
-rw-r--r--plugins/extraction/ExtrOcamlString.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
index 030b486b..a2a6a8fe 100644
--- a/plugins/extraction/ExtrOcamlString.v
+++ b/plugins/extraction/ExtrOcamlString.v
@@ -33,6 +33,7 @@ Extract Constant shift =>
"fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)".
Extract Inlined Constant ascii_dec => "(=)".
+Extract Inlined Constant Ascii.eqb => "(=)".
Extract Inductive string => "char list" [ "[]" "(::)" ].