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.