fixes to work with v8.5 branch.

coq-community · Jun 22, 2015 · 1c36294 · 1c36294
1 parent 138c915
commit 1c36294
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 5 deletions.
diff --git a/theories/Data/Eq.v b/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).
diff --git a/theories/Data/HList.v b/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