From 6bd240fce21c172680a0cec5346b66e08c76418a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 30 Oct 2017 23:48:30 +0100 Subject: [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. --- kernel/term.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/term.mli') diff --git a/kernel/term.mli b/kernel/term.mli index cb782afac..33c6b0b08 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -369,11 +369,11 @@ val mkConstructU : constructor puniverses -> constr val mkConstructUi : (pinductive * int) -> constr [@@ocaml.deprecated "Alias for Constr"] val mkCase : case_info * constr * constr * constr array -> constr -[@@ocaml.deprecated "Alias for Constr"] +[@@ocaml.deprecated "Alias for Constr.mkCase"] val mkFix : fixpoint -> constr -[@@ocaml.deprecated "Alias for Constr"] +[@@ocaml.deprecated "Alias for Constr.mkFix"] val mkCoFix : cofixpoint -> constr -[@@ocaml.deprecated "Alias for Constr"] +[@@ocaml.deprecated "Alias for Constr.mkCoFix"] (** {6 Aliases} *) -- cgit v1.2.3