diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-17 08:23:34 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-17 08:23:34 +0100 |
| commit | dae19c34325b2b98ee0a45ac7908a0c28021ba9e (patch) | |
| tree | e490d5ab864a1baa2457b203d143c60d058a2d77 /theories/Init | |
| parent | 26583840ecb3209b188669fef4204969817f1e32 (diff) | |
| parent | 4fca4ed3b27a51e01370e500cdce756113556ed2 (diff) | |
Merge PR#442: Allow interactive editing of Coq.Init.Logic
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 fb1a7ab1c..9b58c524e 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -572,7 +572,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. |