From e9de7c8232bc696e26114a35b674d221287ea248 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 23 Jan 2012 15:26:00 +0000
Subject: Deleted the only use of BeginSubProof from the standard library.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14938 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/Zeven.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 550b66f781..8e6cc07bf6 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -197,14 +197,14 @@ Qed.
 Lemma Zquot2_quot n : Z.quot2 n = n ÷ 2.
 Proof.
  assert (AUX : forall m, 0 < m -> Z.quot2 m = m ÷ 2).
-  BeginSubproof.
+  {
    intros m Hm.
    apply Z.quot_unique with (if Z.odd m then Z.sgn m else 0).
    now apply Z.lt_le_incl.
    rewrite Z.sgn_pos by trivial.
    destruct (Z.odd m); now split.
    apply Zquot2_odd_eqn.
-  EndSubproof.
+  }
  destruct (Z.lt_trichotomy 0 n) as [POS|[NUL|NEG]].
  - now apply AUX.
  - now subst.
-- 
cgit v1.2.3