From f9f471ce12256e71702a985e8b9a4a6c9dc7bed8 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 17 Dec 2021 13:46:48 -0500 Subject: [PATCH] details --- src/th-data/Sidekick_th_data.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index b6495ffc..e3a026fe 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -321,12 +321,12 @@ module Make(A : ARG) : S with module A = A = struct let (module Act) = acts in let u = - let args = + let sel_args = A.Cstor.ty_args cstor |> Iter.mapi (fun i ty -> A.mk_sel self.tst cstor i t) |> Iter.to_array |> IArray.of_array_unsafe in - A.mk_cstor self.tst cstor args + A.mk_cstor self.tst cstor sel_args in (* proof: resolve [is-c(t) |- t = c(sel-c-0(t), …, sel-c-n(t))] @@ -346,7 +346,6 @@ module Make(A : ARG) : S with module A = A = struct T.Tbl.add self.case_split_done t (); (* no need to decide *) Act.add_clause [Act.mk_lit_nopreproc (A.mk_eq self.tst t u)] proof; - None | _ -> None