Implement formulae parametrized by atomic predicates.

[tatoo.git] / src / sigs.ml

diff --git a/src/sigs.ml b/src/sigs.ml
index a3cf635..1022404 100644 (file)
--- a/src/sigs.ml
+++ b/src/sigs.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-01-30 19:07:19 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-02-05 15:58:13 CET by Kim Nguyen>
 *)
 
 (** This module contains all the signatures of the project, to avoid
@@ -158,6 +158,10 @@ struct
     (** Initializes the internal storage. Any previously hashconsed
         element is discarded. *)
     val init : unit -> unit
+
+    (** Create a dummy (non-hashconsed) node with a boggus identifer
+        and hash *)
+    val dummy : data -> t
   end