aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/extraction.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/extraction/extraction.ml')
-rw-r--r--contrib/extraction/extraction.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 7b2e4c9d7c..7f6821eb87 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -783,6 +783,7 @@ and extract_constant sp =
and eta_expanse ec typ = match ec with
| Emlterm (MLlam _) -> ec
+ | Emlterm (MLfix _) -> ec
| Emlterm a ->
(match extract_type (Global.env()) typ with
| Tmltype (Tarr _, _) ->