From b5e90d92fc52e568f1ed6e65a4b611bdab80e8f5 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Wed, 7 Jun 2017 15:44:41 +0200
Subject: completing a sentence in a comment

---
 lib/pp.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'lib')

diff --git a/lib/pp.mli b/lib/pp.mli
index 7a191b01a8..45834dade5 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -13,6 +13,7 @@
 (* `Pp.t` or `Pp.std_ppcmds` is the main pretty printing document type  *)
 (* in the Coq system. Documents are composed laying out boxes, and      *)
 (* users can add arbitrary tag metadata that backends are free          *)
+(* to interpret.                                                        *)
 (*                                                                      *)
 (* The datatype has a public view to allow serialization or advanced    *)
 (* uses, however regular users are _strongly_ warned againt its use,    *)
-- 
cgit v1.2.3


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 +++++++++++++++++++++-----------------
 lib/flags.mli |  2 +-
 2 files changed, 22 insertions(+), 18 deletions(-)

(limited to 'lib')

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"
diff --git a/lib/flags.mli b/lib/flags.mli
index e2cf09474e..c0aca9c99b 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 = 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
 val compat_version : compat_version ref
 val version_compare : compat_version -> compat_version -> int
 val version_strictly_greater : compat_version -> bool
-- 
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 ++------
 lib/flags.mli | 2 +-
 2 files changed, 3 insertions(+), 7 deletions(-)

(limited to 'lib')

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
diff --git a/lib/flags.mli b/lib/flags.mli
index c0aca9c99b..6e9362681f 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_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current
+type compat_version = VOld | V8_3 | V8_4 | V8_5 | V8_6 | Current
 val compat_version : compat_version ref
 val version_compare : compat_version -> compat_version -> int
 val version_strictly_greater : compat_version -> bool
-- 
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 +-----
 lib/flags.mli | 2 +-
 2 files changed, 2 insertions(+), 6 deletions(-)

(limited to 'lib')

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"
diff --git a/lib/flags.mli b/lib/flags.mli
index 6e9362681f..d6a0eac444 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_3 | V8_4 | V8_5 | V8_6 | Current
+type compat_version = VOld | V8_4 | V8_5 | V8_6 | Current
 val compat_version : compat_version ref
 val version_compare : compat_version -> compat_version -> int
 val version_strictly_greater : compat_version -> bool
-- 
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 +-----
 lib/flags.mli | 2 +-
 2 files changed, 2 insertions(+), 6 deletions(-)

(limited to 'lib')

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"
diff --git a/lib/flags.mli b/lib/flags.mli
index d6a0eac444..0026aba2e3 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_4 | V8_5 | V8_6 | Current
+type compat_version = VOld | V8_5 | V8_6 | Current
 val compat_version : compat_version ref
 val version_compare : compat_version -> compat_version -> int
 val version_strictly_greater : compat_version -> bool
-- 
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 ++++
 lib/flags.mli | 4 ++++
 2 files changed, 8 insertions(+)

(limited to 'lib')

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. *)
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 0026aba2e3..5e78f0a041 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -119,6 +119,10 @@ val is_universe_polymorphism : unit -> bool
 val make_polymorphic_flag : bool -> unit
 val use_polymorphic_flag : unit -> bool
 
+(** Global inductive cumulativity flag. *)
+val make_inductive_cumulativity : bool -> unit
+val is_inductive_cumulativity : unit -> bool
+
 val warn : bool ref
 val make_warn : bool -> unit
 val if_warn : ('a -> unit) -> 'a -> unit
-- 
cgit v1.2.3


From 9c6b492355d82b6346176d884f593bbbf5bde67f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 19 Jun 2017 13:32:40 +0200
Subject: Fix typo in comment.

---
 lib/envars.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/envars.mli b/lib/envars.mli
index edd13447fc..18b7676ce7 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -53,7 +53,7 @@ val coqroot : string
     the order it gets added to the search path. *)
 val coqpath : string list
 
-(** [camlbin ()] is the path to the ocamlfind binary. *)
+(** [camlfind ()] is the path to the ocamlfind binary. *)
 val ocamlfind : unit -> string
 
 (** [camlp4bin ()] is the path to the camlp4 binary. *)
-- 
cgit v1.2.3