From 9a1eb2f4fefcc52f56785f20831e854bb626ae95 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 6 Jul 2016 11:42:35 +0200
Subject: Fix #4793: Coq 8.6 should accept -compat 8.6

We also add a Coq86.v compat file.
---
 doc/stdlib/index-list.html.template | 1 +
 theories/Compat/Coq85.v             | 4 ++++
 theories/Compat/Coq86.v             | 9 +++++++++
 theories/Compat/vo.itarget          | 1 +
 toplevel/coqinit.ml                 | 3 ++-
 toplevel/coqtop.ml                  | 1 +
 6 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 theories/Compat/Coq86.v

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index fb45777e7f..9216c81fcd 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -616,5 +616,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/Compat/AdmitAxiom.v
     theories/Compat/Coq84.v
     theories/Compat/Coq85.v
+    theories/Compat/Coq86.v
   </dd>
 </dl>
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index 1e30ab9197..54621cc1cd 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -8,6 +8,10 @@
 
 (** Compatibility file for making Coq act similar to Coq v8.5 *)
 
+(** Any compatibility changes to make future versions of Coq behave like Coq 8.6
+    are likely needed to make them behave like Coq 8.5. *)
+Require Export Coq.Compat.Coq86.
+
 (* In 8.5, "intros [|]", taken e.g. on a goal "A\/B->C", does not
    behave as "intros [H|H]" but leave instead hypotheses quantified in
    the goal, here producing subgoals A->C and B->C. *)
diff --git a/theories/Compat/Coq86.v b/theories/Compat/Coq86.v
new file mode 100644
index 0000000000..6952fdf199
--- /dev/null
+++ b/theories/Compat/Coq86.v
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \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.6 *)
\ No newline at end of file
diff --git a/theories/Compat/vo.itarget b/theories/Compat/vo.itarget
index 43b197004f..7ffb86ebbd 100644
--- a/theories/Compat/vo.itarget
+++ b/theories/Compat/vo.itarget
@@ -1,3 +1,4 @@
 AdmitAxiom.vo
 Coq84.vo
 Coq85.vo
+Coq86.vo
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 5438b163a3..d9cd574a04 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -130,7 +130,8 @@ let init_ocaml_path () =
         [ "grammar" ]; [ "ide" ]; [ "ltac" ]; ]
 
 let get_compat_version = function
-  | "8.5" -> Flags.Current
+  | "8.6" -> Flags.Current
+  | "8.5" -> Flags.V8_5
   | "8.4" -> Flags.V8_4
   | "8.3" -> Flags.V8_3
   | "8.2" -> Flags.V8_2
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 7c0b9bec21..d141cd8ec1 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -200,6 +200,7 @@ let require () =
 let add_compat_require v =
   match v with
   | Flags.V8_4 -> add_require "Coq.Compat.Coq84"
+  | Flags.V8_5 -> add_require "Coq.Compat.Coq85"
   | _ -> ()
 
 let compile_list = ref ([] : (bool * string) list)
-- 
cgit v1.2.3