From 1ee699431c1791b4486f8bf70b009d1da352e0f5 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 18 Nov 2017 10:43:08 -0500
Subject: [PATCH] Change ProofByReflection to work in Coq 8.6.1

---
 .gitignore          | 1 +
 ProofByReflection.v | 4 +++-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index 0bb7d4b..3090ba6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,6 +10,7 @@
 *.ilg
 *.ind
 Makefile.coq
+Makefile.coq.conf
 *.glob
 *.v.d
 *.vo
diff --git a/ProofByReflection.v b/ProofByReflection.v
index e64c8d2..0eac1cd 100644
--- a/ProofByReflection.v
+++ b/ProofByReflection.v
@@ -497,7 +497,9 @@ Ltac simplify_set :=
   match goal with
   | [ |- context[?X \cup ?Y] ] =>
     let e := reify_set (X \cup Y) in
-    change (X \cup Y) with (setexprDenote e);
+    let Heq := fresh in
+    assert (Heq : X \cup Y = setexprDenote e) by reflexivity;
+    rewrite Heq; clear Heq;
     rewrite normalize_ok; simpl
   end.