summaryrefslogtreecommitdiff
path: root/plugins/extraction/ExtrHaskellString.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/ExtrHaskellString.v')
-rw-r--r--plugins/extraction/ExtrHaskellString.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v
index ac1f6f91..a4a40d3c 100644
--- a/plugins/extraction/ExtrHaskellString.v
+++ b/plugins/extraction/ExtrHaskellString.v
@@ -35,6 +35,8 @@ Extract Inductive ascii => "Prelude.Char"
(Data.Bits.testBit (Data.Char.ord a) 6)
(Data.Bits.testBit (Data.Char.ord a) 7))".
Extract Inlined Constant Ascii.ascii_dec => "(Prelude.==)".
+Extract Inlined Constant Ascii.eqb => "(Prelude.==)".
Extract Inductive string => "Prelude.String" [ "([])" "(:)" ].
Extract Inlined Constant String.string_dec => "(Prelude.==)".
+Extract Inlined Constant String.eqb => "(Prelude.==)".