aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-11 16:07:04 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-10-11 16:07:04 +0200
commitcea76410557f9954c8e15861217bcc4559de9e25 (patch)
tree853557ca2abcce31cc5dbcc77da58df7675f6e48 /configure.ml
parent354ee7d67efda8624cb46e942f2a41211cadd030 (diff)
Remove GeoProof support.
Julien Narboux confirmed that it was dead code (GeoProof is not to be confused with GeoCoq).
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/configure.ml b/configure.ml
index a7acdf532..0952b15f5 100644
--- a/configure.ml
+++ b/configure.ml
@@ -258,7 +258,6 @@ module Prefs = struct
let macintegration = ref true
let browser = ref (None : string option)
let withdoc = ref false
- let geoproof = ref false
let byteonly = ref false
let flambda_flags = ref []
let debug = ref true
@@ -321,8 +320,6 @@ let args_options = Arg.align [
"<command> Use <command> to open URL %s";
"-with-doc", arg_bool Prefs.withdoc,
"(yes|no) Compile the documentation or not";
- "-with-geoproof", arg_bool Prefs.geoproof,
- "(yes|no) Use Geoproof binding or not";
"-byte-only", Arg.Set Prefs.byteonly,
" Compiles only bytecode version of Coq";
"-nodebug", Arg.Clear Prefs.debug,
@@ -1073,7 +1070,6 @@ let write_configml f =
pr_l "flambda_flags" !Prefs.flambda_flags;
pr_i "vo_magic_number" vo_magic;
pr_i "state_magic_number" state_magic;
- pr "let with_geoproof = ref %B\n" !Prefs.geoproof;
pr_s "browser" browser;
pr_s "wwwcoq" !Prefs.coqwebsite;
pr_s "wwwbugtracker" (!Prefs.coqwebsite ^ "bugs/");