From 07646a2dc731beb58d8ae79b5d08b5c04e698bfb Mon Sep 17 00:00:00 2001
From: Christopher Pulte
Date: Thu, 13 Oct 2016 20:29:01 +0100
Subject: make sail-to-lem rewriting passes use dependency analysis, make
 dependency analysis include type information, small pp fix

---
 src/spec_analysis.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/spec_analysis.mli')

diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli
index 6aeb711b..068b3778 100644
--- a/src/spec_analysis.mli
+++ b/src/spec_analysis.mli
@@ -30,3 +30,5 @@ val group_defs : bool -> tannot defs -> ((Nameset.t * Nameset.t) * (tannot def))
 (*reodering definitions, initial functions *)
 (* produce a new ordering for defs, limiting to those listed in the list, which respects dependencies *)
 val restrict_defs : tannot defs -> string list -> tannot defs
+
+val top_sort_defs : tannot defs -> tannot defs
-- 
cgit v1.2.3