From 0e07e69dae3f3f4a99f824533f54a3991aacac6a Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 28 Jun 2016 13:55:20 +0200
Subject: Revert "A new infrastructure for warnings."

This reverts commit 925d258d7d03674c601a1f3832122b3b4b1bc9b0.

I forgot that Jenkins gave me a spurious success when trying to build this PR.
There are a few rough edges to fix, so reverting meanwhile. The Jenkins issue
has been fixed by Matej. Sorry for the noise.
---
 library/libobject.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'library/libobject.mli')

diff --git a/library/libobject.mli b/library/libobject.mli
index 51b9af059f..dbe0de8f8a 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -107,6 +107,7 @@ val subst_object : substitution * obj -> obj
 val classify_object : obj -> obj substitutivity
 val discharge_object : object_name * obj -> obj option
 val rebuild_object : obj -> obj
+val relax : bool -> unit
 
 (** {6 Debug} *)
 
-- 
cgit v1.2.3