From 466ea72b270fb1c4ec7676daf08fa843de196540 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Tue, 7 Feb 2017 20:51:13 -0500
Subject: [PATCH] Finish port to Coq 8.6

---
 Frap.v             | 7 +++++--
 SharedMemory.v     | 5 +++--
 TypesAndMutation.v | 9 +++++++--
 3 files changed, 15 insertions(+), 6 deletions(-)

diff --git a/Frap.v b/Frap.v
index 979aa21..10d7c67 100644
--- a/Frap.v
+++ b/Frap.v
@@ -69,10 +69,13 @@ Ltac same_structure x y :=
 
 Ltac instantiate_obvious1 H :=
   match type of H with
+  | _ ++ _ = _ ++ _ -> _ => fail 1
   | ?x = ?y -> _ =>
-    (same_structure x y; specialize (H eq_refl)) || fail 3
+    (same_structure x y; specialize (H eq_refl))
+    || (has_evar (x, y); fail 3)
   | JMeq.JMeq ?x ?y -> _ =>
-    (same_structure x y; specialize (H JMeq.JMeq_refl)) || fail 3
+    (same_structure x y; specialize (H JMeq.JMeq_refl))
+    || (has_evar (x, y); fail 3)
   | forall x : ?T, _ =>
     match type of T with
     | Prop => fail 1
diff --git a/SharedMemory.v b/SharedMemory.v
index 9f4ad14..6dbd4e1 100644
--- a/SharedMemory.v
+++ b/SharedMemory.v
@@ -1496,6 +1496,7 @@ Proof.
   cases r1; simplify; subst.
   right; eexists (_ :: _); simplify; eauto.
   invert H.
+  first_order; subst; eauto.
   apply IHl1 in H2; first_order; subst; eauto.
 Qed.
 
@@ -1550,7 +1551,7 @@ Proof.
 
   cases x3; simplify.
   invert H.
-  eapply nextAction_det in H0; eauto; propositional; subst.
+  eapply nextAction_det in H0; try eapply H5; eauto; propositional; subst.
   eauto 10.
 
   invert H.
@@ -1574,7 +1575,7 @@ Proof.
 
   cases x3; simplify.
   invert H.
-  eapply nextAction_det in H0; eauto; propositional; subst.
+  eapply nextAction_det in H0; try eapply H5; eauto; propositional; subst.
   eauto 10.
 
   invert H.
diff --git a/TypesAndMutation.v b/TypesAndMutation.v
index 0eb2dc2..965867d 100644
--- a/TypesAndMutation.v
+++ b/TypesAndMutation.v
@@ -236,6 +236,7 @@ Module References.
         | [ H : step _ _ |- _ ] => invert H
         end;
     repeat match goal with
+           | [ H : plug _ _ _ |- _ ] => invert1 H
            | [ H : plug _ _ _ |- _ ] => invert H
            | [ H : step0 _ _ |- _ ] => invert1 H
            | [ H : value _ |- _ ] => invert1 H
@@ -302,8 +303,12 @@ Module References.
          \/ exists he', step (h, e) he'.
   Proof.
     induct 2; t.
-    apply H2 in H8; t.
-    apply H1 in H8; t.
+    match goal with
+    | [ H1 : _ = Some _, H2 : forall l : loc, _ |- _ ] => apply H3 in H8; t
+    end.
+    match goal with
+    | [ H1 : _ = Some _, H2 : forall l : loc, _ |- _ ] => apply H3 in H8; t
+    end.
   Qed.
 
   (* Now, a series of lemmas essentially copied from original type-soundness