Merge branch 'experiments' of Peter_Sewell/sail into mono-experiments

(and fix up monomorphisation)

1 files changed, 6 insertions, 3 deletions

diff --git a/src/constraint.mli b/src/constraint.mli
index 3fb3d2f6..ad75f453 100644
--- a/src/constraint.mli
+++ b/src/constraint.mli
@@ -1,12 +1,15 @@
 type nexp
 type t
 
-type smt_result = Unknown of t list | Unsat of t
-       
+type smt_result = Unknown | Sat | Unsat
+
+val load_digests : unit -> unit
+val save_digests : unit -> unit
+
 val call_z3 : t -> smt_result
 
 val string_of : t -> string
-                                           
+
 val implies : t -> t -> t
 val conj : t -> t -> t
 val disj : t -> t -> t