From 4fca4ed3b27a51e01370e500cdce756113556ed2 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 4 Dec 2016 13:51:15 -0500
Subject: Allow interactive editing of Coq.Init.Logic

Without this change, coqtop complains that I need to require
Coq.Init.Logic to use [replace ... with ... by ...].
---
 theories/Init/Logic.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 85123cc444..504ef95d98 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -553,7 +553,8 @@ Proof.
   intros A P (x & Hp & Huniq); split.
   - intro; exists x; auto.
   - intros (x0 & HPx0 & HQx0) x1 HPx1.
-    replace x1 with x0 by (transitivity x; [symmetry|]; auto).
+    assert (H : x0 = x1) by (transitivity x; [symmetry|]; auto).
+    destruct H.
     assumption.
 Qed.   
 
-- 
cgit v1.2.3