From 2c601b04a08df985f1c3088c5d4668348bfe35d4 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@csail.mit.edu>
Date: Thu, 18 Feb 2016 17:51:58 -0500
Subject: [PATCH] Fixed to work in Coq 8.4, too

---
 Frap.v          |  8 ++++++--
 ModelChecking.v |  2 +-
 Sets.v          | 13 +++++++++++++
 3 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/Frap.v b/Frap.v
index b6ef8e4..b95b0d6 100644
--- a/Frap.v
+++ b/Frap.v
@@ -43,8 +43,12 @@ Ltac invert0 e := invert e; fail.
 Ltac invert1 e := invert0 e || (invert e; []).
 Ltac invert2 e := invert1 e || (invert e; [|]).
 
-Ltac simplify := repeat progress (simpl in *; intros; try autorewrite with core in *; repeat unifyTails);
-                                  repeat (removeDups || doSubtract).
+Ltac simplify := repeat (unifyTails; pose proof I);
+                repeat match goal with
+                       | [ H : True |- _ ] => clear H
+                       end;
+                repeat progress (simpl in *; intros; try autorewrite with core in *);
+                                 repeat (removeDups || doSubtract).
 Ltac propositional := intuition idtac.
 
 Ltac linear_arithmetic := intros;
diff --git a/ModelChecking.v b/ModelChecking.v
index 4ab4dec..61a6fe5 100644
--- a/ModelChecking.v
+++ b/ModelChecking.v
@@ -248,7 +248,7 @@ Ltac model_check_infer :=
   apply multiStepClosure_ok; simplify; model_check_steps.
 
 Ltac model_check_find_invariant :=
-  simplify; eapply invariant_weaken; [ model_check_infer | ].
+  simplify; eapply invariant_weaken; [ model_check_infer | ]; cbv beta in *.
 
 Ltac model_check := model_check_find_invariant; model_check_finish.
 
diff --git a/Sets.v b/Sets.v
index c0b1fc9..d648d44 100644
--- a/Sets.v
+++ b/Sets.v
@@ -169,9 +169,22 @@ Proof.
   unfold constant; intuition eauto using removeDups_fwd, removeDups_bwd.
 Qed.
 
+Ltac someMatch ls :=
+  match ls with
+  | ?x :: ?ls' =>
+    let rec someMatch' ls :=
+        match ls with
+        | x :: _ => idtac
+        | _ :: ?ls' => someMatch' ls'
+        end
+    in someMatch' ls'
+  | _ :: ?ls' => someMatch ls'
+  end.
+
 Ltac removeDups :=
   match goal with
   | [ |- context[constant ?ls] ] =>
+    someMatch ls;
     erewrite (@removeDups_ok _ ls)
       by repeat (apply RdNil
                  || (apply RdNew; [ simpl; intuition congruence | ])