aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-21 19:36:45 +0200
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-27 21:33:39 +0200
commit2826683746569b9d78aa01e319315ab554e1619b (patch)
treeda0933c7169635d9e35003af4d40b0408e7de96d /plugins/extraction
parent8a3cd2fe699540f1ae5a56917d0f6b951f81d731 (diff)
Fix omitted labels in function calls
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/extract_env.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 2b12462ad..322fbcea7 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -657,7 +657,7 @@ let extraction_library is_rec m =
let l = List.rev (environment_until (Some dir_m)) in
let select l (mp,struc) =
if Visit.needed_mp mp
- then (mp, extract_structure env mp no_delta true struc) :: l
+ then (mp, extract_structure env mp no_delta ~all:true struc) :: l
else l
in
let struc = List.fold_left select [] l in