[ci] [coq] Complete 4.06.0 support.

Due to an API change in laglgtk, we need to update CoqIDE. We use a
makefile hack so it can compile with lablgtk < 2.8.16, another option
would be to require 2.8.16 as a minimal dependency.

We also refactor travis to test more lablgtk versions.

We also need to account for improved attribute handling in 4.06.0, in
particular module aliases will propagate the deprecation status.

Fixes #6140.

2 files changed, 95 insertions, 1 deletions

diff --git a/API/API.ml b/API/API.ml
index 9a67e3111..f588fe193 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -20,6 +20,10 @@
 (******************************************************************************)
 module Coq_config = Coq_config
 
+(* Reexporting deprecated symbols throu module aliases triggers a
+   warning in 4.06.0 *)
+[@@@ocaml.warning "-3"]
+
 (******************************************************************************)
 (* Kernel *)
 (******************************************************************************)
diff --git a/API/API.mli b/API/API.mli
index d0564f9ec..cb945179f 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -20,6 +20,10 @@
    See below in the file for their concrete position.
 *)
 
+(* Reexporting deprecated symbols throu module aliases triggers a
+   warning in 4.06.0 *)
+[@@@ocaml.warning "-3"]
+
 (************************************************************************)
 (* Modules from config/                                                 *)
 (************************************************************************)
@@ -300,21 +304,31 @@ sig
   [@@ocaml.deprecated "alias of API.Names.Constant.make3"]
 
   val debug_pr_con : Constant.t -> Pp.t
+  [@@ocaml.deprecated "Alias of Names"]
 
   val debug_pr_mind : MutInd.t -> Pp.t
+  [@@ocaml.deprecated "Alias of Names"]
 
   val pr_con : Constant.t -> Pp.t
+  [@@ocaml.deprecated "Alias of Names"]
 
   val string_of_con : Constant.t -> string
+  [@@ocaml.deprecated "Alias of Names"]
 
   val string_of_mind : MutInd.t -> string
+  [@@ocaml.deprecated "Alias of Names"]
 
   val debug_string_of_mind : MutInd.t -> string
+  [@@ocaml.deprecated "Alias of Names"]
 
   val debug_string_of_con : Constant.t -> string
+  [@@ocaml.deprecated "Alias of Names"]
 
   type identifier = Id.t
+  [@@ocaml.deprecated "Alias of Names"]
+
   module Idset  : Set.S with type elt = identifier and type t = Id.Set.t
+  [@@ocaml.deprecated "Alias of Id.Set.t"]
 
 end
 
@@ -329,6 +343,7 @@ sig
   end
 
   type universe_level = Level.t
+  [@@ocaml.deprecated "Deprecated form, see univ.ml"]
 
   module LSet :
   sig
@@ -343,6 +358,7 @@ sig
   end
 
   type universe = Universe.t
+  [@@ocaml.deprecated "Deprecated form, see univ.ml"]
 
   module Instance :
   sig
@@ -374,6 +390,7 @@ sig
   end
 
   type universe_context = UContext.t
+  [@@ocaml.deprecated "Deprecated form, see univ.ml"]
 
   module AUContext :
   sig
@@ -382,6 +399,7 @@ sig
   end
 
   type abstract_universe_context = AUContext.t
+  [@@ocaml.deprecated "Deprecated form, see univ.ml"]
 
   module CumulativityInfo :
   sig
@@ -389,12 +407,14 @@ sig
   end
 
   type cumulativity_info = CumulativityInfo.t
+  [@@ocaml.deprecated "Deprecated form, see univ.ml"]
 
   module ACumulativityInfo :
   sig
     type t
   end
   type abstract_cumulativity_info = ACumulativityInfo.t
+  [@@ocaml.deprecated "Deprecated form, see univ.ml"]
 
   module ContextSet :
   sig
@@ -408,8 +428,10 @@ sig
   type 'a in_universe_context = 'a * UContext.t
 
   type universe_context_set = ContextSet.t
+  [@@ocaml.deprecated "Deprecated form, see univ.ml"]
 
   type universe_set = LSet.t
+  [@@ocaml.deprecated "Deprecated form, see univ.ml"]
 
   type 'a constraint_function = 'a -> 'a -> Constraint.t -> Constraint.t
 
@@ -586,6 +608,10 @@ val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool
   val mkApp : t * t array -> t
   val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses
 
+  type rec_declaration = Name.t array * types array * constr array
+  type fixpoint = (int array * int) * rec_declaration
+  val mkFix : fixpoint -> constr
+
   val mkConst : Constant.t -> t
   val mkConstU : pconstant -> t
 
@@ -831,8 +857,10 @@ module Term :
 sig
 
   type sorts_family = Sorts.family = InProp | InSet | InType
+  [@@ocaml.deprecated "Alias of Sorts.family"]
 
   type contents = Sorts.contents = Pos | Null
+  [@@ocaml.deprecated "Alias of Sorts.contents"]
 
   type sorts = Sorts.t =
     | Prop of contents
@@ -840,35 +868,48 @@ sig
   [@@ocaml.deprecated "alias of API.Sorts.t"]
 
   type constr = Constr.t
+  [@@ocaml.deprecated "Alias of Constr.t"]
   type types = Constr.t
+  [@@ocaml.deprecated "Alias of Constr.types"]
 
   type metavariable = int
+  [@@ocaml.deprecated "Alias of Constr.metavariable"]
 
   type ('constr, 'types) prec_declaration = Names.Name.t array * 'types array * 'constr array
+  [@@ocaml.deprecated "Alias of Constr.prec_declaration"]
 
   type 'constr pexistential = 'constr Constr.pexistential
+  [@@ocaml.deprecated "Alias of Constr.pexistential"]
+
   type cast_kind = Constr.cast_kind =
                  | VMcast
                  | NATIVEcast
                  | DEFAULTcast
                  | REVERTcast
+  [@@ocaml.deprecated "Alias of Constr.cast_kind"]
 
   type 'a puniverses = 'a Univ.puniverses
+  [@@ocaml.deprecated "Alias of Constr.puniverses"]
   type pconstant = Names.Constant.t puniverses
+  [@@ocaml.deprecated "Alias of Constr.pconstant"]
   type pinductive = Names.inductive puniverses
+  [@@ocaml.deprecated "Alias of Constr.pinductive"]
   type pconstructor = Names.constructor puniverses
+  [@@ocaml.deprecated "Alias of Constr.pconstructor"]
   type case_style = Constr.case_style =
     | LetStyle
     | IfStyle
     | LetPatternStyle
     | MatchStyle
     | RegularStyle
+  [@@ocaml.deprecated "Alias of Constr.case_style"]
 
   type case_printing = Constr.case_printing =
     { ind_tags  : bool list;
       cstr_tags : bool list array;
       style     : case_style
     }
+  [@@ocaml.deprecated "Alias of Constr.case_printing"]
 
   type case_info = Constr.case_info =
     { ci_ind        : Names.inductive;
@@ -877,12 +918,15 @@ sig
       ci_cstr_nargs : int array;
       ci_pp_info    : case_printing
     }
+  [@@ocaml.deprecated "Alias of Constr.case_info"]
 
   type ('constr, 'types) pfixpoint =
     (int array * int) * ('constr, 'types) prec_declaration
+  [@@ocaml.deprecated "Alias of Constr.pfixpoint"]
 
   type ('constr, 'types) pcofixpoint =
     int * ('constr, 'types) prec_declaration
+  [@@ocaml.deprecated "Alias of Constr.pcofixpoint"]
 
   type ('constr, 'types, 'sort, 'univs) kind_of_term = ('constr, 'types, 'sort, 'univs) Constr.kind_of_term =
      | Rel       of int
@@ -902,11 +946,17 @@ sig
      | Fix       of ('constr, 'types) pfixpoint
      | CoFix     of ('constr, 'types) pcofixpoint
      | Proj      of Names.Projection.t * 'constr
+  [@@ocaml.deprecated "Alias of Constr.kind_of_term"]
   type existential = Constr.existential_key * constr array
+  [@@ocaml.deprecated "Alias of Constr.existential"]
   type rec_declaration = Names.Name.t array * constr array * constr array
+  [@@ocaml.deprecated "Alias of Constr.rec_declaration"]
   type fixpoint = (int array * int) * rec_declaration
+  [@@ocaml.deprecated "Alias of Constr.fixpoint"]
   type cofixpoint = int * rec_declaration
+  [@@ocaml.deprecated "Alias of Constr.cofixpoint"]
   val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term
+  [@@ocaml.deprecated "Alias of Constr.kind"]
   val applistc : constr -> constr list -> constr
 
   val applist : constr * constr list -> constr
@@ -914,29 +964,52 @@ sig
 
   val mkArrow : types -> types -> constr
   val mkRel : int -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkVar : Names.Id.t -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
 
   val mkMeta : Constr.metavariable -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
 
   val mkEvar : existential -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkSort : Sorts.t -> types
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkProp : types
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkSet  : types
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkType : Univ.Universe.t -> types
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkCast : constr * cast_kind * constr -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkProd : Names.Name.t * types * types -> types
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkLambda : Names.Name.t * types * constr -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkLetIn : Names.Name.t * constr * types * constr -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkApp : constr * constr array -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkConst : Names.Constant.t -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkProj : Names.Projection.t * constr -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkInd : Names.inductive -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkConstruct : Names.constructor -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkConstructU : Names.constructor puniverses -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkConstructUi : (pinductive * int) -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkCase : case_info * constr * constr * constr array -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkFix : fixpoint -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
   val mkCoFix : cofixpoint -> constr
+  [@@ocaml.deprecated "Alias of similarly named Constr function"]
+
   val mkNamedLambda : Names.Id.t -> types -> constr -> constr
   val mkNamedLetIn : Names.Id.t -> constr -> types -> constr -> constr
   val mkNamedProd : Names.Id.t -> types -> types -> types
@@ -975,26 +1048,37 @@ sig
   val isApp : constr -> bool
 
   val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a
+  [@@ocaml.deprecated "Alias of Constr.fold"]
 
   val eq_constr : constr -> constr -> bool
+  [@@ocaml.deprecated "Alias of Constr.equal"]
 
   val hash_constr : constr -> int
+  [@@ocaml.deprecated "Alias of Constr.hash"]
+
   val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
   val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
   val prod_applist : constr -> constr list -> constr
   exception DestKO
   val map_constr : (constr -> constr) -> constr -> constr
+  [@@ocaml.deprecated "Alias of Constr.map"]
 
   val mkIndU : pinductive -> constr
+  [@@ocaml.deprecated "Alias of Constr.mkIndU"]
   val mkConstU : pconstant -> constr
+  [@@ocaml.deprecated "Alias of Constr.mkConstU"]
   val map_constr_with_binders :
     ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
+  [@@ocaml.deprecated "Alias of Constr.map_with_binders"]
+
   val iter_constr : (constr -> unit) -> constr -> unit
+  [@@ocaml.deprecated "Alias of Constr.iter."]
 
   (* Quotients away universes: really needed?
    * Can't we just call eq_c_univs_infer and discard the inferred csts?
    *)
   val eq_constr_nounivs : constr -> constr -> bool
+  [@@ocaml.deprecated "Alias of Constr.qe_constr_nounivs."]
 
   type ('constr, 'types) kind_of_type =
     | SortType   of Sorts.t
@@ -1009,13 +1093,16 @@ sig
   [@@ocaml.deprecated "alias of API.Sorts.is_prop"]
 
   type existential_key = Constr.existential_key
+  [@@ocaml.deprecated "Alias of Constr.existential_key"]
 
   val family_of_sort : Sorts.t -> Sorts.family
+  [@@ocaml.deprecated "Alias of Sorts.family"]
 
   val compare : constr -> constr -> int
+  [@@ocaml.deprecated "Alias of Constr.compare."]
 
   val constr_ord : constr -> constr -> int
-  [@@ocaml.deprecated "alias of API.Term.compare"]
+  [@@ocaml.deprecated "alias of Term.compare"]
 
   val destInd : constr -> Names.inductive puniverses
   val univ_of_sort : Sorts.t -> Univ.Universe.t
@@ -1027,6 +1114,8 @@ sig
   val destFix : constr -> fixpoint
 
   val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
+  [@@ocaml.deprecated "Alias of Constr.compare_head."]
+
 end
 
 module Mod_subst :
@@ -1673,6 +1762,7 @@ sig
     | LetPatternStyle
     | MatchStyle
     | RegularStyle (** infer printing form from number of constructor *)
+  [@@ocaml.deprecated "Alias for Constr.case_style."]
 
   type 'a cast_type =
                     | CastConv of 'a