Merge remote-tracking branch 'remotes/origin/coq-8.10' into coq-8.11

3 files changed, 117 insertions, 32 deletions

diff --git a/src/SMT_terms.v b/src/SMT_terms.v
index 1f16538..66936cf 100644
--- a/src/SMT_terms.v
+++ b/src/SMT_terms.v
@@ -274,13 +274,13 @@ Module Typ.
       match t with
       | TFArray ti te =>
         existT (fun ty : Type => CompDec ty)
-               (@farray (projT1 (interp_compdec_aux ti))
-                        (projT1 (interp_compdec_aux te))
+               (@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
-                  (projT1 (interp_compdec_aux ti))
-                  (projT1 (interp_compdec_aux te)))
+                  (type_compdec (projT2 (interp_compdec_aux ti)))
+                  (type_compdec (projT2 (interp_compdec_aux te))))
       | Tindex i =>
         existT (fun ty : Type => CompDec ty)
                (te_carrier (t_i .[ i])) (te_compdec (t_i .[ i]))
@@ -293,7 +293,7 @@ Module Typ.
     Definition interp_compdec (t:type) : CompDec (projT1 (interp_compdec_aux t)) :=
       projT2 (interp_compdec_aux t).
 
-    Definition interp (t:type) : Type := projT1 (interp_compdec_aux t).
+    Definition interp (t:type) : Type := type_compdec (interp_compdec t).
 
 
     Definition interp_ftype (t:ftype) :=
@@ -304,21 +304,21 @@ Module Typ.
     Definition dec_interp (t:type) : DecType (interp t).
     Proof.
       unfold interp.
-      destruct (interp_compdec_aux t) as [x c]. simpl.
+      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_aux t) as [x c]. simpl.
+      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_aux t) as [x c]. simpl.
+      destruct (interp_compdec t) as [x c]. simpl.
       apply Comp.
     Defined.
 
@@ -349,7 +349,7 @@ Module Typ.
           eqb_of_compdec c x y = true <-> x = y.
       Proof.
         intros x y.
-        destruct c as [[E HE] O C I].
+        destruct c as [TY [E HE] O C I].
         unfold eqb_of_compdec.
         simpl. now rewrite HE.
       Qed.
diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v
index 7d8e994..de20723 100644
--- a/src/array/Array_checker.v
+++ b/src/array/Array_checker.v
@@ -1227,21 +1227,91 @@ Section certif.
     subst.
     specialize (Atom.Bval_inj2 t_i v_typed2' (v_vald2) (@diff (Typ.interp t_i v_typed2') (Typ.interp t_i v_typec1')
              (@EqbToDecType
-                _
+                (@projT1 Type (fun ty : Type => CompDec ty)
+                   (Typ.interp_compdec_aux t_i v_typed2'))
                 (@eqbtype_of_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)
+                   ((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 i))
+                             (te_compdec (@get typ_compdec t_i 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')
-                (projT2
+                (@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
-                                (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux ti))
-                                (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux te))
+                                (@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))
@@ -1253,10 +1323,20 @@ Section certif.
                                    (@projT2 Type (fun ty : Type => CompDec ty)
                                       (interp_compdec_aux te))))
                              (@SMT_classes_instances.FArray_compdec
-                                (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux ti))
-                                (@projT1 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)))
+                                (@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 i))
@@ -1268,14 +1348,16 @@ Section certif.
                            @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
+                           @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)
+                             (BVList.BITVECTOR_LIST.bitvector n)
+                             (SMT_classes_instances.BV_compdec n)
                        end) v_typed2'))) (Typ.dec_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)).
+             (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 (H5 Htid2''').
     rewrite <- H5.
     specialize (Atom.Bval_inj2 t_i v_typed2' (v_vale2) (v_vald2)).
diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v
index d314aa0..53d5dcc 100644
--- a/src/classes/SMT_classes.v
+++ b/src/classes/SMT_classes.v
@@ -148,27 +148,30 @@ Class Inhabited T := {
 (** * CompDec: Merging all previous classes *)
 
 Class CompDec T := {
-  Eqb :> EqbType T;             (* This is redundant since implied by Comp, but it actually allows us to choose a specific equality function *)
-  Ordered :> OrdType T;
-  Comp :> @Comparable T Ordered;
-  Inh :> Inhabited T
+  ty := T;                      (* This is redundant for performance reasons *)
+  Eqb :> EqbType ty;             (* This is redundant since implied by Comp, but it actually allows us to choose a specific equality function *)
+  Ordered :> OrdType ty;
+  Comp :> @Comparable ty Ordered;
+  Inh :> Inhabited ty
 }.
 
 
 Instance eqbtype_of_compdec t `{c: CompDec t} : (EqbType t) :=
-  let (eqb, _, _, _) := c in eqb.
+  let (_, eqb, _, _, _) := c in eqb.
 
 Instance ord_of_compdec t `{c: CompDec t} : (OrdType t) :=
-  let (_, ord, _, _) := c in ord.
+  let (_, _, ord, _, _) := c in ord.
 
 Instance inh_of_compdec t `{c: CompDec t} : (Inhabited t) :=
-  let (_, _, _, inh) := c in inh.
+  let (_, _, _, _, inh) := c in inh.
 
 Instance comp_of_compdec t `{c: CompDec t} : @Comparable t (ord_of_compdec t).
   destruct c; trivial.
 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
   | {| eqb := eqb |} => eqb
@@ -178,7 +181,7 @@ Definition eqb_of_compdec {t} (c : CompDec t) : t -> t -> bool :=
 Lemma compdec_eq_eqb {T:Type} {c : CompDec T} : forall x y : T,
     x = y <-> eqb_of_compdec c x y = true.
 Proof.
-  intros x y. destruct c as [[E HE] O C I]. unfold eqb_of_compdec. simpl. now rewrite HE.
+  intros x y. destruct c as [TY [E HE] O C I]. unfold eqb_of_compdec. simpl. now rewrite HE.
 Qed.
 
 Hint Resolve