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 +-
 2 files changed, 1 insertion(+), 2 deletions(-)

(limited to 'src')

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
-- 
cgit