diff options
| author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-12-08 23:38:28 (GMT) |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-12-09 15:41:18 (GMT) |
| commit | 04a6362feb6cbfaa00be4d001dee2b390d0ff21c (patch) | |
| tree | e9f0a840016064441cf2d9a5e06ecbb2c7461177 | |
| parent | 81266e09faeceda6dd14af823e8ff13748c881bc (diff) | |
| download | coq-v8.3.zip coq-v8.3.tar.gz coq-v8.3.tar.bz2 | |
Adding support for OCaml 4.06.0 (option -unsafe-string needed).refs/pull/6360/headv8.3
And other minor changes.
Cherry-pick from v8.4 (7f2240f).
| -rw-r--r-- | INSTALL | 1 | ||||
| -rwxr-xr-x | configure | 11 |
2 files changed, 10 insertions, 2 deletions
@@ -49,6 +49,7 @@ WHAT DO YOU NEED ? with the corresponding version of Objective Caml, however avoiding version 5.00) + - The num library if with Objective Caml version 4.06.0 or later - GNU Make version 3.81 or later ( @@ -105,6 +105,7 @@ coq_debug_flag_opt= coq_profile_flag= coq_annotate_flag= coq_warning_flag= +coq_safe_string_flag= best_compiler=opt cflags="-fno-defer-pop -Wall -Wno-unused" natdynlink=yes @@ -444,11 +445,17 @@ case $CAMLVERSION in CAMLP4COMPAT="-loc loc" echo "Warning: OCaml 4.02.0 suffers from a bug inducing" echo "very slow compilation times";; - ?*) + 4.0[0-5]*) # From 4.03.0, 4.00.0's warning 31, irrelevant for us, is fatal when activated CAMLP4COMPAT="-loc loc" coq_warning_flag="-w -31" echo "You have Objective-Caml $CAMLVERSION. Good!";; + ?*) + # From 4.06.0 + CAMLP4COMPAT="-loc loc" + coq_warning_flag="-w -31" + coq_safe_string_flag=-unsafe-string + echo "You have Objective-Caml $CAMLVERSION. Good!";; *) echo "I found the Objective-Caml compiler but cannot find its version number!" echo "Is it installed properly?" @@ -1120,7 +1127,7 @@ CAMLOPTLINK="$nativecamlc" CAMLMKTOP="$ocamlmktopexec" # Caml flags -CAMLFLAGS=-rectypes $coq_annotate_flag $coq_warning_flag +CAMLFLAGS=-rectypes $coq_annotate_flag $coq_warning_flag $coq_safe_string_flag # Compilation debug flags CAMLDEBUG=$coq_debug_flag |