diff options
| -rw-r--r-- | doc/stdlib/index-list.html.template | 1 | ||||
| -rw-r--r-- | lib/flags.ml | 6 | ||||
| -rw-r--r-- | lib/flags.mli | 2 | ||||
| -rw-r--r-- | theories/Compat/Coq86.v | 2 | ||||
| -rw-r--r-- | theories/Compat/Coq87.v | 9 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 3 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 1 |
7 files changed, 21 insertions, 3 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 48f82f2d9..48048b7a0 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -591,5 +591,6 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/AdmitAxiom.v theories/Compat/Coq85.v theories/Compat/Coq86.v + theories/Compat/Coq87.v </dd> </dl> diff --git a/lib/flags.ml b/lib/flags.ml index 5d9d9dcf5..0bce22f58 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -106,7 +106,7 @@ let we_are_parsing = ref false (* Current means no particular compatibility consideration. For correct comparisons, this constructor should remain the last one. *) -type compat_version = VOld | V8_5 | V8_6 | Current +type compat_version = VOld | V8_5 | V8_6 | V8_7 | Current let compat_version = ref Current @@ -120,6 +120,9 @@ let version_compare v1 v2 = match v1, v2 with | V8_6, V8_6 -> 0 | V8_6, _ -> -1 | _, V8_6 -> 1 + | V8_7, V8_7 -> 0 + | V8_7, _ -> -1 + | _, V8_7 -> 1 | Current, Current -> 0 let version_strictly_greater v = version_compare !compat_version v > 0 @@ -129,6 +132,7 @@ let pr_version = function | VOld -> "old" | V8_5 -> "8.5" | V8_6 -> "8.6" + | V8_7 -> "8.7" | Current -> "current" (* Translate *) diff --git a/lib/flags.mli b/lib/flags.mli index e63f1ec26..eb4c37a54 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -77,7 +77,7 @@ val raw_print : bool ref (* Univ print flag, never set anywere. Maybe should belong to Univ? *) val univ_print : bool ref -type compat_version = VOld | V8_5 | V8_6 | Current +type compat_version = VOld | V8_5 | V8_6 | V8_7 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool diff --git a/theories/Compat/Coq86.v b/theories/Compat/Coq86.v index f46460886..34061ddd6 100644 --- a/theories/Compat/Coq86.v +++ b/theories/Compat/Coq86.v @@ -7,5 +7,7 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.6 *) +Require Export Coq.Compat.Coq87. + Require Export Coq.extraction.Extraction. Require Export Coq.funind.FunInd. diff --git a/theories/Compat/Coq87.v b/theories/Compat/Coq87.v new file mode 100644 index 000000000..61e911678 --- /dev/null +++ b/theories/Compat/Coq87.v @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Compatibility file for making Coq act similar to Coq v8.7 *) diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index f61416dde..326ef5471 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -127,7 +127,8 @@ let init_ocaml_path () = List.iter add_subdir Coq_config.all_src_dirs let get_compat_version ?(allow_old = true) = function - | "8.7" -> Flags.Current + | "8.8" -> Flags.Current + | "8.7" -> Flags.V8_7 | "8.6" -> Flags.V8_6 | "8.5" -> Flags.V8_5 | ("8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 08c235023..d09171bc8 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -209,6 +209,7 @@ let add_compat_require v = match v with | Flags.V8_5 -> add_require "Coq.Compat.Coq85" | Flags.V8_6 -> add_require "Coq.Compat.Coq86" + | Flags.V8_7 -> add_require "Coq.Compat.Coq87" | Flags.VOld | Flags.Current -> () let compile_list = ref ([] : (bool * string) list) |