aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/ExtrHaskellString.v
diff options
context:
space:
mode:
authorWilliam Lawvere2017-07-01 22:10:46 -0700
committerWilliam Lawvere2017-07-01 22:10:46 -0700
commit80649ebaba75838bfd28ae78822cd2c078da4b23 (patch)
treeac29ab5edd3921dbee1c2256737347fd1542dc67 /plugins/extraction/ExtrHaskellString.v
parentc2942e642ee6f83cc997f9a2510cdb7446a65cb4 (diff)
parent35e0f327405fb659c7ec5f9f7d26ea284aa45810 (diff)
Merge remote-tracking branch 'upstream/trunk' into trunk
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 3558f4f254..ac1f6f9130 100644
--- a/plugins/extraction/ExtrHaskellString.v
+++ b/plugins/extraction/ExtrHaskellString.v
@@ -2,6 +2,8 @@
* Special handling of ascii and strings for extraction to Haskell.
*)
+Require Coq.extraction.Extraction.
+
Require Import Ascii.
Require Import String.