From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- plugins/extraction/ExtrOcamlString.v | 1 + 1 file changed, 1 insertion(+) (limited to 'plugins/extraction/ExtrOcamlString.v') 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" [ "[]" "(::)" ]. -- cgit v1.2.3