Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12

6 files changed, 134 insertions, 211 deletions

diff --git a/src/PropToBool.v b/src/PropToBool.v
index 6d12c99..31f8b2d 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -59,7 +59,7 @@ Ltac prop2bool :=
         | _ =>
           let p := fresh "p" in
           assert (p:CompDec t);
-          [ auto with typeclass_instances
+          [ try (exact _)       (* Use the typeclass machinery *)
           | rewrite (@compdec_eq_eqb _ p)
           ]
         end
@@ -172,7 +172,7 @@ Ltac prop2bool_hyp H :=
     | _ =>
       let Hcompdec := fresh "Hcompdec" in
       assert (Hcompdec: CompDec A);
-      [ auto with typeclass_instances | ]
+      [ try (exact _) | ]
     end
   | false => idtac
   end;
@@ -223,7 +223,7 @@ Ltac remove_compdec_hyp H :=
     | _ =>
       let c := fresh "c" in
       assert (c : CompDec A);
-      [ auto with typeclass_instances
+      [ try (exact _)
       | let H1 := fresh in
         assert (H1 := H c); clear H; assert (H := H1); clear H1;
         remove_compdec_hyp H ]
diff --git a/src/SMT_terms.v b/src/SMT_terms.v
index f536bd6..b5716c4 100644
--- a/src/SMT_terms.v
+++ b/src/SMT_terms.v
@@ -275,14 +275,18 @@ Module Typ.
     Fixpoint interp_compdec_aux (t:type) : {ty: Type & CompDec ty} :=
       match t with
       | TFArray ti te =>
+        let iti := interp_compdec_aux ti in
+        let ite := interp_compdec_aux te in
+        let cti := projT2 iti in
+        let cte := projT2 ite in
+        let tti := type_compdec cti in
+        let tte := type_compdec cte in
         existT (fun ty : Type => CompDec ty)
-               (@farray (type_compdec (projT2 (interp_compdec_aux ti)))
-                        (type_compdec (projT2 (interp_compdec_aux te)))
-                        (@ord_of_compdec _ (projT2 (interp_compdec_aux ti)))
-                        (@inh_of_compdec _ (projT2 (interp_compdec_aux te))))
-               (FArray_compdec
-                  (type_compdec (projT2 (interp_compdec_aux ti)))
-                  (type_compdec (projT2 (interp_compdec_aux te))))
+               (@farray tti
+                        tte
+                        (@ord_of_compdec tti cti)
+                        (@inh_of_compdec tte cte))
+               (FArray_compdec tti tte)
       | Tindex i =>
         existT (fun ty : Type => CompDec ty)
                (te_carrier (t_i .[of_Z (Z.of_N i)])) (te_compdec (t_i .[of_Z (Z.of_N i)]))
@@ -292,10 +296,10 @@ Module Typ.
       | TBV n => existT (fun ty : Type => CompDec ty) (BITVECTOR_LIST.bitvector n) (BV_compdec n)
       end.
 
-    Definition interp_compdec (t:type) : CompDec (projT1 (interp_compdec_aux t)) :=
-      projT2 (interp_compdec_aux t).
+    Definition interp (t:type) : Type := type_compdec (projT2 (interp_compdec_aux t)).
 
-    Definition interp (t:type) : Type := type_compdec (interp_compdec t).
+    Definition interp_compdec (t:type) : CompDec (interp t) :=
+      projT2 (interp_compdec_aux t).
 
 
     Definition interp_ftype (t:ftype) :=
@@ -303,40 +307,17 @@ Module Typ.
       (interp (snd t)) (fst t).
 
 
-    Definition dec_interp (t:type) : DecType (interp t).
-    Proof.
-      unfold interp.
-      destruct (interp_compdec t) as [x c]. simpl.
-      apply EqbToDecType.
-    Defined.
-
-    Instance ord_interp (t:type) : OrdType (interp t).
-    Proof.
-      unfold interp.
-      destruct (interp_compdec t) as [x c]. simpl.
-      apply Ordered.
-    Defined.
-
-    Instance comp_interp (t:type) : Comparable (interp t).
-    Proof.
-      unfold interp, ord_interp.
-      destruct (interp_compdec t) as [x c]. simpl.
-      apply Comp.
-    Defined.
-
-
-    Definition inh_interp (t:type) : Inhabited (interp t).
-      unfold interp.
-      destruct (interp_compdec t).
-      apply Inh.
-    Defined.
+    Global Instance dec_interp (t:type) : DecType (interp t) :=
+      (@EqbToDecType _ (@eqbtype_of_compdec (interp t) (interp_compdec t))).
 
-    Definition inhabitant_interp (t:type) : interp t := @default_value _ (inh_interp _).
+    Global Instance ord_interp (t:type) : OrdType (interp t) :=
+      @ord_of_compdec (interp t) (interp_compdec t).
 
+    Global Instance comp_interp (t:type) : Comparable (interp t) :=
+      @comp_of_compdec (interp t) (interp_compdec t).
 
-    Hint Resolve
-         dec_interp comp_interp ord_interp
-         inh_interp interp_compdec : typeclass_instances.
+    Global Instance inh_interp (t:type) : Inhabited (interp t) :=
+      @inh_of_compdec (interp t) (interp_compdec t).
 
 
     (* Boolean equality over interpretation of a btype *)
@@ -1525,13 +1506,25 @@ Qed.
            apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_shr s)
          | BO_select ti te => apply_binop (Typ.TFArray ti te) ti te FArray.select
          | BO_diffarray ti te =>
-           apply_binop (Typ.TFArray ti te) (Typ.TFArray ti te) ti (@FArray.diff (Typ.interp t_i ti) (Typ.interp t_i te) (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti))) (ord_of_compdec _) _ (Typ.dec_interp t_i te) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i ti) (Typ.inh_interp t_i te))
+           let iti := Typ.interp_compdec_aux t_i ti in
+           let ite := Typ.interp_compdec_aux t_i te in
+           let cti := projT2 iti in
+           let cte := projT2 ite in
+           let tti := type_compdec cti in
+           let tte := type_compdec cte in
+           apply_binop (Typ.TFArray ti te) (Typ.TFArray ti te) ti (@FArray.diff tti tte (@EqbToDecType _ (@eqbtype_of_compdec tti cti)) (@ord_of_compdec tti cti) (@comp_of_compdec tti cti) (@EqbToDecType _ (@eqbtype_of_compdec tte cte)) (@ord_of_compdec tte cte) (@comp_of_compdec tte cte) (@inh_of_compdec tti cti) (@inh_of_compdec tte cte))
          end.
 
       Definition interp_top o :=
          match o with
          | TO_store ti te =>
-           apply_terop (Typ.TFArray ti te) ti te (Typ.TFArray ti te) (@FArray.store (Typ.interp t_i ti) (Typ.interp t_i te) (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti))) (ord_of_compdec _) _ (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i te))
+           let iti := Typ.interp_compdec_aux t_i ti in
+           let ite := Typ.interp_compdec_aux t_i te in
+           let cti := projT2 iti in
+           let cte := projT2 ite in
+           let tti := type_compdec cti in
+           let tte := type_compdec cte in
+           apply_terop (Typ.TFArray ti te) ti te (Typ.TFArray ti te) (@FArray.store tti tte (@EqbToDecType _ (@eqbtype_of_compdec tti cti)) (@ord_of_compdec tti cti) (@comp_of_compdec tti cti) (@ord_of_compdec tte cte) (@comp_of_compdec tte cte) (@inh_of_compdec tte cte))
          end.
 
       Fixpoint compute_interp ty acc l :=
@@ -1966,9 +1959,9 @@ Qed.
         rewrite !Typ.cast_refl.
         intros.
         exists ((@FArray.diff (Typ.interp t_i t') (Typ.interp t_i te)
-             (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t')))
-             (ord_of_compdec _)
-             (comp_of_compdec _) (Typ.dec_interp t_i te) (Typ.ord_interp t_i te)
+             (Typ.dec_interp t_i t')
+             (Typ.ord_interp t_i t')
+             (Typ.comp_interp t_i t') (Typ.dec_interp t_i te) (Typ.ord_interp t_i te)
              (Typ.comp_interp t_i te) (Typ.inh_interp t_i t') (Typ.inh_interp t_i te) x1 x2)); auto.
 
         (* Ternary operatores *)
@@ -1990,11 +1983,7 @@ Qed.
         intros.
         rewrite !Typ.cast_refl.
         intros.
-        exists ((@FArray.store (Typ.interp t_i ti') (Typ.interp t_i te')
-             (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti')))
-             (ord_of_compdec _)
-             (comp_of_compdec _) (Typ.ord_interp t_i te') (Typ.comp_interp t_i te')
-             (Typ.inh_interp t_i te') x1 x2 x3)); auto.
+        exists (@FArray.store (Typ.interp t_i ti') (Typ.interp t_i te') (Typ.dec_interp t_i ti') (Typ.ord_interp t_i ti') (Typ.comp_interp t_i ti') (Typ.ord_interp t_i te') (Typ.comp_interp t_i te') (Typ.inh_interp t_i te') x1 x2 x3); auto.
 
         (* N-ary operators *)
         destruct op as [A]; simpl; intros [ | | | | | ]; try discriminate; simpl; intros _; case (compute_interp A nil ha).
@@ -2475,12 +2464,7 @@ Qed.
           simpl; try (exists true; auto); intro k1;
             case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) (Typ.TFArray ti te)) as [k2| ];
             simpl; try (exists true; reflexivity).
-        exists ((@FArray.diff (Typ.interp t_i ti) (Typ.interp t_i te)
-             (@EqbToDecType _ (@eqbtype_of_compdec _(Typ.interp_compdec t_i ti)))
-             (ord_of_compdec _)
-             (comp_of_compdec _) (Typ.dec_interp t_i te) (Typ.ord_interp t_i te)
-             (Typ.comp_interp t_i te) (Typ.inh_interp t_i ti) (Typ.inh_interp t_i te)
-             (k1 (Typ.interp t_i) x) (k2 (Typ.interp t_i) y))); auto.
+        exists ((@FArray.diff (Typ.interp t_i ti) (Typ.interp t_i te) (Typ.dec_interp t_i ti) (Typ.ord_interp t_i ti) (Typ.comp_interp t_i ti) (Typ.dec_interp t_i te) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i ti) (Typ.inh_interp t_i te) (k1 (Typ.interp t_i) x) (k2 (Typ.interp t_i) y))); auto.
 
         (* Ternary operators *)
         intros [ti te] h1 h2 h3; simpl; rewrite !andb_true_iff; intros [[H1 H2] H3];
@@ -2494,9 +2478,9 @@ Qed.
             case (Typ.cast (v_type Typ.type interp_t (a .[ h3])) te) as [k3| ];
             simpl; try (exists true; reflexivity).
          exists (@FArray.store (Typ.interp t_i ti) (Typ.interp t_i te)
-             (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti)))
-             (ord_of_compdec _)
-             (comp_of_compdec _) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te)
+             (Typ.dec_interp t_i ti)
+             (Typ.ord_interp t_i ti)
+             (Typ.comp_interp t_i ti) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te)
              (Typ.inh_interp t_i te) (k1 (Typ.interp t_i) x) (k2 (Typ.interp t_i) y)
              (k3 (Typ.interp t_i) z)); auto.
 
diff --git a/src/Tactics.v b/src/Tactics.v
index edf2f19..5be62cc 100644
--- a/src/Tactics.v
+++ b/src/Tactics.v
@@ -69,8 +69,8 @@ Ltac get_hyps :=
 
 (** Tactics in bool *)
 
-Tactic Notation "verit_bool_base_auto" constr(h) := verit_bool_base h; auto with typeclass_instances.
-Tactic Notation "verit_bool_no_check_base_auto" constr(h) := verit_bool_no_check_base h; auto with typeclass_instances.
+Tactic Notation "verit_bool_base_auto" constr(h) := verit_bool_base h; try (exact _).
+Tactic Notation "verit_bool_no_check_base_auto" constr(h) := verit_bool_no_check_base h; try (exact _).
 
 Tactic Notation "verit_bool" constr(h) :=
   let Hs := get_hyps in
diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v
index f95c282..83b04bb 100644
--- a/src/array/Array_checker.v
+++ b/src/array/Array_checker.v
@@ -382,7 +382,7 @@ Section certif.
         intros.
         specialize (Atom.Bval_inj2 t_i (Typ.TFArray t0 t)
           (@store _ _
-                  (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t0)))
+                  (Typ.dec_interp t_i t0)
                _ _ _ (Typ.comp_interp t_i t) _
                v_val2 v_val3 v_val4) v_val0).
         intros. specialize (H18 H6).
@@ -682,7 +682,7 @@ Section certif.
           rewrite H25a, H25b, H10. intros.
           specialize (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2)
             (@store _ _
-                    (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t1)))
+                    (Typ.dec_interp t_i t1)
                    _ _ _ (Typ.comp_interp t_i t2) _
                    v_vale1 v_vale2 v_vale3) (v_vald1')).
           intro H25. specialize (H25 Htid1').
@@ -839,7 +839,7 @@ Section certif.
           rewrite H25a, H25b, H10. intros.
           specialize (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2)
             (@store _ _
-                   (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t1)))
+                   (Typ.dec_interp t_i t1)
                    _ _ _ (Typ.comp_interp t_i t2) _
                    v_vale1 v_vale2 v_vale3) (v_valc1')).
           intro H25. specialize (H25 Htic1').
@@ -1176,7 +1176,7 @@ Section certif.
     rewrite !Typ.cast_refl. intros.
 
     specialize (Atom.Bval_inj2 t_i t0 (@diff _ _
-       (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t0)))
+       (Typ.dec_interp t_i t0)
        _ _ (Typ.dec_interp t_i v_typec2') _ (Typ.comp_interp t_i v_typec2') (Typ.inh_interp t_i t0) _
        v_valf1 v_valf2) (v_vald2')).
     intros. specialize (H28 Htid2').
@@ -1221,141 +1221,88 @@ Section certif.
     apply negb_true_iff.
     apply Typ.i_eqb_spec_false.
     subst.
-    specialize (Atom.Bval_inj2 t_i v_typed2' (v_vald2) (@diff (Typ.interp t_i v_typed2') (Typ.interp t_i v_typec1')
+
+    specialize (Atom.Bval_inj2 t_i v_typed2' v_vald2 (@diff
+             _
+             _
              (@EqbToDecType
-                (@projT1 Type (fun ty : Type => CompDec ty)
-                   (Typ.interp_compdec_aux t_i v_typed2'))
+                (@type_compdec
+                   (@projT1 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typed2'))
+                   (@projT2 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typed2')))
                 (@eqbtype_of_compdec
+                   (@type_compdec
+                      (@projT1 Type (fun ty : Type => CompDec ty)
+                         (Typ.interp_compdec_aux t_i v_typed2'))
+                      (@projT2 Type (fun ty : Type => CompDec ty)
+                         (Typ.interp_compdec_aux t_i v_typed2')))
+                   (@projT2 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typed2'))))
+             (@ord_of_compdec
+                (@type_compdec
                    (@projT1 Type (fun ty : Type => CompDec ty)
                       (Typ.interp_compdec_aux t_i v_typed2'))
-                   (Typ.interp_compdec t_i v_typed2')))
-             (@ord_of_compdec (Typ.interp t_i v_typed2')
+                   (@projT2 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typed2')))
                 (@projT2 Type (fun ty : Type => CompDec ty)
-                   ((fix interp_compdec_aux (t : Typ.type) :
-                       @sigT Type (fun ty : Type => CompDec ty) :=
-                       match t return (@sigT Type (fun ty : Type => CompDec ty)) with
-                       | Typ.TFArray ti te =>
-                           @existT Type (fun ty : Type => CompDec ty)
-                             (@farray
-                                (@type_compdec
-                                   (@projT1 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux ti))
-                                   (@projT2 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux ti)))
-                                (@type_compdec
-                                   (@projT1 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux te))
-                                   (@projT2 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux te)))
-                                (@ord_of_compdec
-                                   (@projT1 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux ti))
-                                   (@projT2 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux ti)))
-                                (@inh_of_compdec
-                                   (@projT1 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux te))
-                                   (@projT2 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux te))))
-                             (@SMT_classes_instances.FArray_compdec
-                                (@type_compdec
-                                   (@projT1 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux ti))
-                                   (@projT2 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux ti)))
-                                (@type_compdec
-                                   (@projT1 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux te))
-                                   (@projT2 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux te)))
-                                (@projT2 Type (fun ty : Type => CompDec ty)
-                                   (interp_compdec_aux ti))
-                                (@projT2 Type (fun ty : Type => CompDec ty)
-                                   (interp_compdec_aux te)))
-                       | Typ.Tindex i =>
-                           @existT Type (fun ty : Type => CompDec ty)
-                             (te_carrier (@get typ_compdec t_i (of_Z (Z.of_N i))))
-                             (te_compdec (@get typ_compdec t_i (of_Z (Z.of_N i))))
-                       | Typ.TZ =>
-                           @existT Type (fun ty : Type => CompDec ty) BinNums.Z
-                             SMT_classes_instances.Z_compdec
-                       | Typ.Tbool =>
-                           @existT Type (fun ty : Type => CompDec ty) bool
-                             SMT_classes_instances.bool_compdec
-                       | Typ.Tpositive =>
-                           @existT Type (fun ty : Type => CompDec ty)
-                             BinNums.positive SMT_classes_instances.Positive_compdec
-                       | Typ.TBV n =>
-                           @existT Type (fun ty : Type => CompDec ty)
-                             (BVList.BITVECTOR_LIST.bitvector n)
-                             (SMT_classes_instances.BV_compdec n)
-                       end) v_typed2')))
-             (@comp_of_compdec (Typ.interp t_i v_typed2')
+                   (Typ.interp_compdec_aux t_i v_typed2')))
+             (@comp_of_compdec
+                (@type_compdec
+                   (@projT1 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typed2'))
+                   (@projT2 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typed2')))
+                (@projT2 Type (fun ty : Type => CompDec ty)
+                   (Typ.interp_compdec_aux t_i v_typed2')))
+             (@EqbToDecType
+                (@type_compdec
+                   (@projT1 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typec1'))
+                   (@projT2 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typec1')))
+                (@eqbtype_of_compdec
+                   (@type_compdec
+                      (@projT1 Type (fun ty : Type => CompDec ty)
+                         (Typ.interp_compdec_aux t_i v_typec1'))
+                      (@projT2 Type (fun ty : Type => CompDec ty)
+                         (Typ.interp_compdec_aux t_i v_typec1')))
+                   (@projT2 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typec1'))))
+             (@ord_of_compdec
+                (@type_compdec
+                   (@projT1 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typec1'))
+                   (@projT2 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typec1')))
+                (@projT2 Type (fun ty : Type => CompDec ty)
+                   (Typ.interp_compdec_aux t_i v_typec1')))
+             (@comp_of_compdec
+                (@type_compdec
+                   (@projT1 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typec1'))
+                   (@projT2 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typec1')))
+                (@projT2 Type (fun ty : Type => CompDec ty)
+                   (Typ.interp_compdec_aux t_i v_typec1')))
+             (@inh_of_compdec
+                (@type_compdec
+                   (@projT1 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typed2'))
+                   (@projT2 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typed2')))
+                (@projT2 Type (fun ty : Type => CompDec ty)
+                   (Typ.interp_compdec_aux t_i v_typed2')))
+             (@inh_of_compdec
+                (@type_compdec
+                   (@projT1 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typec1'))
+                   (@projT2 Type (fun ty : Type => CompDec ty)
+                      (Typ.interp_compdec_aux t_i v_typec1')))
                 (@projT2 Type (fun ty : Type => CompDec ty)
-                   ((fix interp_compdec_aux (t : Typ.type) :
-                       @sigT Type (fun ty : Type => CompDec ty) :=
-                       match t return (@sigT Type (fun ty : Type => CompDec ty)) with
-                       | Typ.TFArray ti te =>
-                           @existT Type (fun ty : Type => CompDec ty)
-                             (@farray
-                                (@type_compdec
-                                   (@projT1 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux ti))
-                                   (@projT2 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux ti)))
-                                (@type_compdec
-                                   (@projT1 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux te))
-                                   (@projT2 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux te)))
-                                (@ord_of_compdec
-                                   (@projT1 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux ti))
-                                   (@projT2 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux ti)))
-                                (@inh_of_compdec
-                                   (@projT1 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux te))
-                                   (@projT2 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux te))))
-                             (@SMT_classes_instances.FArray_compdec
-                                (@type_compdec
-                                   (@projT1 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux ti))
-                                   (@projT2 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux ti)))
-                                (@type_compdec
-                                   (@projT1 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux te))
-                                   (@projT2 Type (fun ty : Type => CompDec ty)
-                                      (interp_compdec_aux te)))
-                                (@projT2 Type (fun ty : Type => CompDec ty)
-                                   (interp_compdec_aux ti))
-                                (@projT2 Type (fun ty : Type => CompDec ty)
-                                   (interp_compdec_aux te)))
-                       | Typ.Tindex i =>
-                           @existT Type (fun ty : Type => CompDec ty)
-                             (te_carrier (@get typ_compdec t_i (of_Z (Z.of_N i))))
-                             (te_compdec (@get typ_compdec t_i (of_Z (Z.of_N i))))
-                       | Typ.TZ =>
-                           @existT Type (fun ty : Type => CompDec ty) BinNums.Z
-                             SMT_classes_instances.Z_compdec
-                       | Typ.Tbool =>
-                           @existT Type (fun ty : Type => CompDec ty) bool
-                             SMT_classes_instances.bool_compdec
-                       | Typ.Tpositive =>
-                           @existT Type (fun ty : Type => CompDec ty)
-                             BinNums.positive SMT_classes_instances.Positive_compdec
-                       | Typ.TBV n =>
-                           @existT Type (fun ty : Type => CompDec ty)
-                             (BVList.BITVECTOR_LIST.bitvector n)
-                             (SMT_classes_instances.BV_compdec n)
-                       end) v_typed2'))) (Typ.dec_interp t_i v_typec1')
-             (Typ.ord_interp t_i v_typec1') (Typ.comp_interp t_i v_typec1')
-             (Typ.inh_interp t_i v_typed2') (Typ.inh_interp t_i v_typec1') v_valf1
-             v_valf2)).
-    intros. specialize (H4 Htid2''').
-    rewrite <- H4.
+                   (Typ.interp_compdec_aux t_i v_typec1'))) v_valf1 v_valf2)).
+    intros H5. specialize (H5 Htid2''').
+    rewrite <- H5.
     specialize (Atom.Bval_inj2 t_i v_typed2' (v_vale2) (v_vald2)).
     intros.
 
diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v
index 53d5dcc..9ee394b 100644
--- a/src/classes/SMT_classes.v
+++ b/src/classes/SMT_classes.v
@@ -156,16 +156,16 @@ Class CompDec T := {
 }.
 
 
-Instance eqbtype_of_compdec t `{c: CompDec t} : (EqbType t) :=
+Global Instance eqbtype_of_compdec {t} `{c: CompDec t} : (EqbType t) :=
   let (_, eqb, _, _, _) := c in eqb.
 
-Instance ord_of_compdec t `{c: CompDec t} : (OrdType t) :=
+Global Instance ord_of_compdec {t} `{c: CompDec t} : (OrdType t) :=
   let (_, _, ord, _, _) := c in ord.
 
-Instance inh_of_compdec t `{c: CompDec t} : (Inhabited t) :=
+Global Instance inh_of_compdec {t} `{c: CompDec t} : (Inhabited t) :=
   let (_, _, _, _, inh) := c in inh.
 
-Instance comp_of_compdec t `{c: CompDec t} : @Comparable t (ord_of_compdec t).
+Global Instance comp_of_compdec {t} `{c: CompDec t} : @Comparable t (ord_of_compdec (t:=t)).
   destruct c; trivial.
 Defined.
 
@@ -173,7 +173,7 @@ Defined.
 Definition type_compdec {ty:Type} (cd : CompDec ty) := ty.
 
 Definition eqb_of_compdec {t} (c : CompDec t) : t -> t -> bool :=
-  match eqbtype_of_compdec t with
+  match eqbtype_of_compdec (t:=t) with
   | {| eqb := eqb |} => eqb
   end.
 
@@ -184,12 +184,6 @@ Proof.
   intros x y. destruct c as [TY [E HE] O C I]. unfold eqb_of_compdec. simpl. now rewrite HE.
 Qed.
 
-Hint Resolve
-     ord_of_compdec
-     inh_of_compdec
-     comp_of_compdec
-     eqbtype_of_compdec : typeclass_instances.
-
 
 Record typ_compdec : Type := Typ_compdec {
   te_carrier : Type;
diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v
index 5020185..1c8b2f6 100644
--- a/src/classes/SMT_classes_instances.v
+++ b/src/classes/SMT_classes_instances.v
@@ -747,5 +747,3 @@ Section prod.
   |}.
 
 End prod.
-
-Hint Resolve unit_compdec bool_compdec Z_compdec Nat_compdec Positive_compdec BV_compdec FArray_compdec int63_compdec option_compdec list_compdec prod_compdec : typeclass_instances.