From 12ba49ae5f679c9412e90b0d3bbf47880962248e Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Thu, 10 Jun 2021 13:00:00 -0400
Subject: [PATCH] more doc

---
 src/core/Sidekick_core.ml | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 9dcdac68..b2b2a515 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -51,6 +51,7 @@ module CC_view = struct
     | Opaque t -> f_t t
 end
 
+(** Main representation of Terms and Types *)
 module type TERM = sig
   module Fun : sig
     type t
@@ -117,6 +118,12 @@ module type LIT = sig
   val pp : t Fmt.printer
 end
 
+(** Actions provided to the congruence closure.
+
+    The congruence closure must be able to propagate literals when
+    it detects that they are true or false; it must also
+    be able to create conflicts when the set of (dis)equalities
+    is inconsistent *)
 module type CC_ACTIONS = sig
   module T : TERM
   module P : PROOF