From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- toplevel/auto_ind_decl.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel/auto_ind_decl.mli') diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index b6c66a1e..fa5c6148 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -21,7 +21,7 @@ exception EqUnknown of string exception UndefinedCst of string exception InductiveWithProduct exception InductiveWithSort -exception ParameterWithoutEquality of constant +exception ParameterWithoutEquality of Globnames.global_reference exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported -- cgit v1.2.3