diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-12-04 13:51:15 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-21 20:51:35 -0500 |
| commit | 4fca4ed3b27a51e01370e500cdce756113556ed2 (patch) | |
| tree | 6e9f95429894c9ceafef1de6db8209dd6afbb8a9 /theories/Init | |
| parent | d9d8977cf213f0d4b2e8d324c759c23df58ba457 (diff) | |
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 ...].
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Logic.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 85123cc44..504ef95d9 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. |