aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_makefile.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coq_makefile.ml4')
-rw-r--r--tools/coq_makefile.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index a7c89e7af..450796a53 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -418,7 +418,7 @@ let main_targets vfiles mlfiles other_targets inc =
let all_target (vfiles, mlfiles, sps, sds) inc =
let special_targets = List.filter (fun (n,_,_) -> not (is_genrule n)) sps in
- let other_targets = List.map (fun x,_,_ -> x) special_targets @ sds in
+ let other_targets = List.map (function x,_,_ -> x) special_targets @ sds in
section "Definition of the \"all\" target.";
main_targets vfiles mlfiles other_targets inc;
custom sps;