fix bug #2447 in congruence

1 files changed, 32 insertions, 2 deletions

diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index 50e3624d0a..ba95ebb59e 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -20,10 +20,40 @@ type rule=
 and proof =
     private {p_lhs:term;p_rhs:term;p_rule:rule}
 
+(** Proof smart constructors *)
+
+val prefl:term -> proof
+
+val pcongr: proof -> proof -> proof
+
+val ptrans: proof -> proof -> proof
+
+val psym: proof -> proof
+
+val pax : (Ccalgo.term * Ccalgo.term) Ccalgo.Constrhash.t ->
+           Ccalgo.Constrhash.key -> proof
+
+val psymax :  (Ccalgo.term * Ccalgo.term) Ccalgo.Constrhash.t ->
+           Ccalgo.Constrhash.key -> proof
+
+val pinject :  proof -> pconstructor -> int -> int -> proof
+
+(** Proof building functions *)
+
+val equal_proof : forest -> int -> int -> proof
+
+val edge_proof : forest -> (int*int)*equality -> proof
+
+val path_proof : forest -> int -> ((int*int)*equality) list -> proof
+
+val congr_proof :  forest -> int -> int -> proof
+
+val ind_proof : forest -> int -> pa_constructor -> int -> pa_constructor -> proof
+
+(** Main proof building function *)
+
 val build_proof :
   forest ->
   [ `Discr of int * pa_constructor * int * pa_constructor
   | `Prove of int * int ] -> proof
 
-
-