From fac9967dcfcfd771cbcf17b364b324bc19587159 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Wed, 5 May 2021 17:33:45 +0200
Subject: CompDec on interpreted type

---
 src/PropToBool.v                 |  1 -
 src/trace/smtBtype.ml            |  2 +-
 unit-tests/Tests_verit_tactics.v | 35 +++++++++++++++++++++++++++++++++++
 3 files changed, 36 insertions(+), 2 deletions(-)

diff --git a/src/PropToBool.v b/src/PropToBool.v
index 00cba37..c77647d 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -221,7 +221,6 @@ Ltac remove_compdec_hyp H :=
       assert (H1 := H p'); clear H; assert (H := H1); clear H1;
       remove_compdec_hyp H
     | _ =>
-      idtac 1;
       let c := fresh "c" in
       assert (c : CompDec A);
       [ auto with typeclass_instances
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
index 1e05dc4..2194a57 100644
--- a/src/trace/smtBtype.ml
+++ b/src/trace/smtBtype.ml
@@ -310,6 +310,6 @@ let of_coq_compdec reify t compdec =
                Hashtbl.add reify.tbl t res;
                res
          )
-      | _ -> assert false
+      | _ -> ty
   with Not_found ->
     declare_compdec reify t compdec
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index bd4082f..daff848 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -1294,3 +1294,38 @@ Section CompDecHypotheses.
   Proof. verit. Qed.
 
 End CompDecHypotheses.
+
+
+Section CompDecOnInterpretedType.
+  Variable A : Type.
+  Variable H : CompDec A.
+  Variable x : A.
+  Variable l2 : list A.
+  Variable Hcompdec : CompDec (list A).
+  Variable H1 : (forall (H3 H4 : A) (H5 H6 : list A),
+        eqb_of_compdec Hcompdec (H3 :: H5) (H4 :: H6) --->
+        eqb_of_compdec H H4 H3 && eqb_of_compdec Hcompdec H6 H5 = true).
+  Variable H2 : (forall (H3 : A) (H4 : list A),
+        eqb_of_compdec Hcompdec nil (H3 :: H4) ---> false = true).
+  Variable Hcompdec0 : CompDec (list bool).
+  Variable H7_bool : (forall (H3 : bool) (H4 H5 : list bool),
+             eqb_of_compdec Hcompdec0 ((H3 :: H4) ++ H5)%list (H3 :: H4 ++ H5) = true).
+  Variable H7_A : (forall (H3 : A) (H4 H5 : list A),
+          eqb_of_compdec Hcompdec ((H3 :: H4) ++ H5)%list (H3 :: H4 ++ H5) = true).
+  Variable H6_bool : (forall H3 : list bool,
+             eqb_of_compdec Hcompdec0 (nil ++ H3)%list H3 = true).
+  Variable H6_A : (forall H3 : list A, eqb_of_compdec Hcompdec (nil ++ H3)%list H3 = true).
+  Variable c : CompDec bool.
+  Variable search : forall {A : Type} {H: CompDec A}, A -> list A -> bool.
+  Arguments search {_ _} _ _.
+  Variable H5_bool : (forall (H3 H4 : bool) (H5 : list bool),
+             search H3 (H4 :: H5) <---> eqb_of_compdec c H3 H4 || search H3 H5 = true).
+  Variable H5_A : (forall (H3 H4 : A) (H5 : list A),
+          search H3 (H4 :: H5) <---> eqb_of_compdec H H3 H4 || search H3 H5 = true).
+  Variable H4_bool : (forall H3 : bool, search H3 nil <---> false = true).
+  Variable H4_A : (forall H3 : A, search H3 nil <---> false = true).
+
+  Goal search x l2 <---> search x l2 = true.
+  Proof. verit. Qed.
+
+End CompDecOnInterpretedType.
-- 
cgit