fixes to work with v8.5 branch.

Author: Gregory Malecha

theories/Data/Eq.v

@@ -98,7 +98,7 @@ Hint Rewrite eq_sym_eq_sym : eq_rw.
 Ltac autorewrite_eq_rw :=
   repeat progress (autorewrite with eq_rw;
                    repeat match goal with
-                            | |- context [ match ?X return _ -> _ with
+                            | |- context [ match ?X in @eq _ _ _ return _ -> _ with
                                              | eq_refl => _
                                            end ] => rewrite (eq_Arr_eq X)
                           end).

theories/Data/HList.v

@@ -658,10 +658,8 @@ Section hlist.
   Proof.
     induction ls; simpl; intros; try congruence.
     { destruct n; intuition. }
-    { destruct n; simpl; try solve [ intuition congruence ].
-      { unfold value. intuition congruence. }
-      { specialize (IHls n).
-        forward. } }
+    { destruct n; simpl; try solve [ unfold value; intuition congruence ].
+      specialize (IHls n). forward. }
   Qed.
 
   Lemma nth_error_get_hlist_nth_weaken