Merge remote-tracking branch 'upstream/trunk' into trunk

4 files changed, 24 insertions, 23 deletions

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. *)
diff --git a/lib/flags.ml b/lib/flags.ml
index 6a3b7a4261..46bbba8e55 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -106,35 +106,27 @@ 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_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_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
-  | V8_2 -> "8.2"
-  | V8_3 -> "8.3"
-  | V8_4 -> "8.4"
+  | VOld -> "old"
   | V8_5 -> "8.5"
   | V8_6 -> "8.6"
   | Current -> "current"
@@ -157,7 +149,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
@@ -171,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 e2cf09474e..5e78f0a041 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_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
@@ -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
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,    *)