From 0253fc47be156d0d87cccda32c5bb90bc37960da Mon Sep 17 00:00:00 2001
From: Carst Tankink <carst.tankink@inria.fr>
Date: Thu, 9 Oct 2014 15:39:08 +0200
Subject: When loading libraries, feed back dependencies.

These dependencies between files can be used by UIs to guide compilation
and reloading of files.

FileDependency (Some "/foo.v", "/bar.v")  means foo depends on bar.
FileDependency (None, "/bar.v") means the current file depends on bar.
---
 lib/feedback.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'lib/feedback.mli')

diff --git a/lib/feedback.mli b/lib/feedback.mli
index 775f71e9e..d6d77b7cc 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -44,6 +44,7 @@ type feedback_content =
   | ProcessingInMaster
   | Goals of Loc.t * string
   | StructuredGoals of Loc.t * xml
+  | FileDependency of string option * string
   | FileLoaded of string * string
   | Message of message
 
-- 
cgit v1.2.3