1 files changed, 1 insertions, 4 deletions
diff --git a/configure.ml b/configure.ml
index 1d2003501..1a851ef45 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1022,15 +1022,12 @@ let write_configml f =
   let pr_s = pr "let %s = %S\n" in
   let pr_b = pr "let %s = %B\n" in
   let pr_i = pr "let %s = %d\n" in
-  let pr_o s o = pr "let %s = %s\n" s
-    (match o with None -> "None" | Some d -> sprintf "Some %S" d)
-  in
   pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n";
   pr "(* Exact command that generated this file: *)\n";
   pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv));
   pr_b "local" !Prefs.local;
   pr "let vmbyteflags = ["; List.iter (pr "%S;") vmbyteflags; pr "]\n";
-  pr_o "coqlib" (if !Prefs.local then None else Some coqlib);
+  pr_s "coqlib" coqlib;
   pr_s "configdir" configdir;
   pr_s "datadir" datadir;
   pr_s "docdir" docdir;