From 80dfe0cb64285f58dfe2eebd7319c747c70d3d6b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 7 Apr 2017 09:49:21 +0200
Subject: Add a version to be used when parsing compatibility notations
 mentioning old versions.

---
 lib/flags.ml | 38 +++++++++++++++++++++-----------------
 1 file changed, 21 insertions(+), 17 deletions(-)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index 6a3b7a4261..682e2e4df1 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -106,32 +106,36 @@ 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 = V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current
+type compat_version = VOld | V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current
 
 let compat_version = ref Current
 
 let version_compare v1 v2 = match v1, v2 with
-| V8_2, V8_2 -> 0
-| V8_2, (V8_3 | V8_4 | V8_5 | V8_6 | Current) -> -1
-| V8_3, V8_2 -> 1
-| V8_3, V8_3 -> 0
-| V8_3, (V8_4 | V8_5 | V8_6 | Current) -> -1
-| V8_4, (V8_2 | V8_3) -> 1
-| V8_4, V8_4 -> 0
-| V8_4, (V8_5 | V8_6 | Current) -> -1
-| V8_5, (V8_2 | V8_3 | V8_4) -> 1
-| V8_5, V8_5 -> 0
-| V8_5, (V8_6 | Current) -> -1
-| V8_6, (V8_2 | V8_3 | V8_4 | V8_5) -> 1
-| V8_6, V8_6 -> 0
-| V8_6, Current -> -1
-| Current, Current -> 0
-| Current, (V8_2 | V8_3 | V8_4 | V8_5 | V8_6) -> 1
+  | VOld, VOld -> 0
+  | VOld, _ -> -1
+  | _, VOld -> 1
+  | V8_2, V8_2 -> 0
+  | V8_2, _ -> -1
+  | _, V8_2 -> 1
+  | V8_3, V8_3 -> 0
+  | V8_3, _ -> -1
+  | _, V8_3 -> 1
+  | V8_4, V8_4 -> 0
+  | V8_4, _ -> -1
+  | _, V8_4 -> 1
+  | V8_5, V8_5 -> 0
+  | V8_5, _ -> -1
+  | _, V8_5 -> 1
+  | V8_6, V8_6 -> 0
+  | V8_6, _ -> -1
+  | _, V8_6 -> 1
+  | Current, Current -> 0
 
 let version_strictly_greater v = version_compare !compat_version v > 0
 let version_less_or_equal v = not (version_strictly_greater v)
 
 let pr_version = function
+  | VOld -> "old"
   | V8_2 -> "8.2"
   | V8_3 -> "8.3"
   | V8_4 -> "8.4"
-- 
cgit v1.2.3


From 571c319ed536cb2757176d3ae4007a75f5d3b04d Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 22 Nov 2016 17:08:14 +0100
Subject: Remove support for Coq 8.2.

---
 lib/flags.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index 682e2e4df1..c4a97bd12e 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_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current
+type compat_version = VOld | V8_3 | V8_4 | V8_5 | V8_6 | Current
 
 let compat_version = ref Current
 
@@ -114,9 +114,6 @@ let version_compare v1 v2 = match v1, v2 with
   | VOld, VOld -> 0
   | VOld, _ -> -1
   | _, VOld -> 1
-  | V8_2, V8_2 -> 0
-  | V8_2, _ -> -1
-  | _, V8_2 -> 1
   | V8_3, V8_3 -> 0
   | V8_3, _ -> -1
   | _, V8_3 -> 1
@@ -136,7 +133,6 @@ let version_less_or_equal v = not (version_strictly_greater v)
 
 let pr_version = function
   | VOld -> "old"
-  | V8_2 -> "8.2"
   | V8_3 -> "8.3"
   | V8_4 -> "8.4"
   | V8_5 -> "8.5"
@@ -161,7 +157,7 @@ let is_verbose () = not !quiet
 
 let auto_intros = ref true
 let make_auto_intros flag = auto_intros := flag
-let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros
+let is_auto_intros () = !auto_intros
 
 let universe_polymorphism = ref false
 let make_universe_polymorphism b = universe_polymorphism := b
-- 
cgit v1.2.3


From daf5335b18c926d7130cd28e50f00cc49c4011f6 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 22 Nov 2016 17:12:58 +0100
Subject: Remove support for Coq 8.3.

---
 lib/flags.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index c4a97bd12e..d738e3df18 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_3 | V8_4 | V8_5 | V8_6 | Current
+type compat_version = VOld | V8_4 | V8_5 | V8_6 | Current
 
 let compat_version = ref Current
 
@@ -114,9 +114,6 @@ let version_compare v1 v2 = match v1, v2 with
   | VOld, VOld -> 0
   | VOld, _ -> -1
   | _, VOld -> 1
-  | V8_3, V8_3 -> 0
-  | V8_3, _ -> -1
-  | _, V8_3 -> 1
   | V8_4, V8_4 -> 0
   | V8_4, _ -> -1
   | _, V8_4 -> 1
@@ -133,7 +130,6 @@ let version_less_or_equal v = not (version_strictly_greater v)
 
 let pr_version = function
   | VOld -> "old"
-  | V8_3 -> "8.3"
   | V8_4 -> "8.4"
   | V8_5 -> "8.5"
   | V8_6 -> "8.6"
-- 
cgit v1.2.3


From bcaf9af83363f3e1a1c588271e5038984ee1760b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sat, 8 Apr 2017 07:04:56 +0200
Subject: Remove support for Coq 8.4.

---
 lib/flags.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index d738e3df18..13539bced3 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_4 | V8_5 | V8_6 | Current
+type compat_version = VOld | V8_5 | V8_6 | Current
 
 let compat_version = ref Current
 
@@ -114,9 +114,6 @@ let version_compare v1 v2 = match v1, v2 with
   | VOld, VOld -> 0
   | VOld, _ -> -1
   | _, VOld -> 1
-  | V8_4, V8_4 -> 0
-  | V8_4, _ -> -1
-  | _, V8_4 -> 1
   | V8_5, V8_5 -> 0
   | V8_5, _ -> -1
   | _, V8_5 -> 1
@@ -130,7 +127,6 @@ let version_less_or_equal v = not (version_strictly_greater v)
 
 let pr_version = function
   | VOld -> "old"
-  | V8_4 -> "8.4"
   | V8_5 -> "8.5"
   | V8_6 -> "8.6"
   | Current -> "current"
-- 
cgit v1.2.3


From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 27 Apr 2017 20:16:35 +0200
Subject: Fix bugs and add an option for cumulativity

---
 lib/flags.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index 13539bced3..46bbba8e55 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -163,6 +163,10 @@ let use_polymorphic_flag () =
 let make_polymorphic_flag b =
   local_polymorphic_flag := Some b
 
+let inductive_cumulativity = ref false
+let make_inductive_cumulativity b = inductive_cumulativity := b
+let is_inductive_cumulativity () = !inductive_cumulativity
+
 (** [program_mode] tells that Program mode has been activated, either
     globally via [Set Program] or locally via the Program command prefix. *)
 
-- 
cgit v1.2.3