From 7b2b11486f5cc0f77cdf220df63d0939cec64866 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 30 Mar 2021 16:00:36 -0400 Subject: [PATCH] dbg --- src/th-data/Sidekick_th_data.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 1800cb4c..cf8f20a8 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -235,7 +235,7 @@ module Make(A : ARG) : S with module A = A = struct let merge cc n1 c1 n2 c2 e_n1_n2 : _ result = Log.debugf 5 - (fun k->k "(@[%s.merge@ (@[:c1 %a %a@])@ (@[:c2 %a %a@])@])" + (fun k->k "(@[%s.merge@ (@[:c1 %a@ %a@])@ (@[:c2 %a@ %a@])@])" name N.pp n1 pp c1 N.pp n2 pp c2); (* build full explanation of why the constructor terms are equal *) (* TODO: have a sort of lemma (injectivity) here to justify this in the proof *)