- Added two new introduction patterns with the following temptative syntaxes:

  - "*" implements Arthur Charguéraud's "introv"
  - "**" works as "; intros" (see also "*" in ssreflect).
- Simplifying the proof of Z_eq_dec, as suggested by Frédéric Blanqui.
- Shy attempt to seize the opportunity to clean Zarith_dec but Coq's
  library is really going anarchically (see a summary of the various
  formulations of total order, dichotomy of order and decidability of
  equality and in stdlib-project.tex in branch V8revised-theories).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12171 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 3 deletions

diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 076bceba4..af281b73f 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -266,12 +266,19 @@ Definition Pmax (p p' : positive) := match Pcompare p p' Eq with
  end.
 
 (**********************************************************************)
-(** Miscellaneous properties of binary positive numbers *)
+(** Decidability of equality on binary positive numbers *)
 
-Lemma ZL11 : forall p:positive, p = 1 \/ p <> 1.
+Lemma positive_eq_dec : forall x y: positive, {x = y} + {x <> y}.
 Proof.
-  intros x; case x; intros; (left; reflexivity) || (right; discriminate).
+  decide equality.
+Defined.
+
+(* begin hide *)
+Corollary ZL11 : forall p:positive, p = 1 \/ p <> 1.
+Proof.
+  intro; edestruct positive_eq_dec; eauto.
 Qed.
+(* end hide *)
 
 (**********************************************************************)
 (** Properties of successor on binary positive numbers *)