- 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

11 files changed, 113 insertions, 71 deletions

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 35107c808..8724b0bfd 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -82,6 +82,7 @@ type intro_pattern_expr =
   | IntroRewrite of bool
   | IntroIdentifier of identifier
   | IntroFresh of identifier
+  | IntroForthcoming of bool
   | IntroAnonymous
 and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list
 
@@ -92,6 +93,8 @@ let rec pr_intro_pattern (_,pat) = match pat with
   | IntroRewrite false -> str "<-"
   | IntroIdentifier id -> pr_id id
   | IntroFresh id -> str "?" ++ pr_id id
+  | IntroForthcoming true -> str "*"
+  | IntroForthcoming false -> str "**"
   | IntroAnonymous -> str "?"
 
 and pr_or_and_intro_pattern = function
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 92c7db36f..9072456c3 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -39,6 +39,7 @@ type intro_pattern_expr =
   | IntroRewrite of bool
   | IntroIdentifier of identifier
   | IntroFresh of identifier
+  | IntroForthcoming of bool
   | IntroAnonymous
 and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index e370b693f..c0a3f2e77 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -256,7 +256,9 @@ GEXTEND Gram
   naming_intropattern:
     [ [ prefix = pattern_ident -> loc, IntroFresh prefix
       | "?" -> loc, IntroAnonymous
-      | id = ident -> loc, IntroIdentifier id ] ]
+      | id = ident -> loc, IntroIdentifier id
+      | "*" -> loc, IntroForthcoming true
+      | "**" -> loc, IntroForthcoming false ] ]
   ;
   intropattern_modifier:
     [ [ IDENT "_eqn"; 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 18322504e..a494738f9 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -75,6 +75,7 @@ let mlexpr_of_intro_pattern = function
   | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >>
   | Genarg.IntroAnonymous -> <:expr< Genarg.IntroAnonymous >>
   | Genarg.IntroFresh id -> <:expr< Genarg.IntroFresh (mlexpr_of_ident $dloc$ id) >>
+  | Genarg.IntroForthcoming b -> <:expr< Genarg.IntroForthcoming (mlexpr_of_bool $dloc$ b) >>
   | Genarg.IntroIdentifier id ->
       <:expr< Genarg.IntroIdentifier (mlexpr_of_ident $dloc$ id) >>
   | Genarg.IntroOrAndPattern _ | Genarg.IntroRewrite _ ->
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 9f5da99a7..7b0e5e0ef 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -74,7 +74,7 @@ let mkBranches c1 c2 =
 
 let solveNoteqBranch side = 
   tclTHEN (choose_noteq side)
-    (tclTHEN (intro_force true)
+    (tclTHEN introf
       (onLastHypId (fun id -> Extratactics.h_discrHyp id)))
 
 let h_solveNoteqBranch side =
diff --git a/tactics/inv.ml b/tactics/inv.ml
index a0d1d2783..ae76e6b26 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -378,7 +378,7 @@ let rewrite_equations_gene othin neqns ba gl =
 let rec get_names allow_conj (loc,pat) = match pat with
   | IntroWildcard ->
       error "Discarding pattern not allowed for inversion equations."
-  | IntroAnonymous ->
+  | IntroAnonymous | IntroForthcoming _ ->
       error "Anonymous pattern not allowed for inversion equations."
   | IntroFresh _ ->
       error "Fresh pattern not allowed for inversion equations."
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index cbc1c6ce2..c21a4c080 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -485,7 +485,7 @@ let rec intern_intro_pattern lf ist = function
       loc, IntroIdentifier (intern_ident lf ist id)
   | loc, IntroFresh id ->
       loc, IntroFresh (intern_ident lf ist id)
-  | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _)
+  | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _ | IntroForthcoming _)
       as x -> x
 
 and intern_or_and_intro_pattern lf ist =
@@ -1362,7 +1362,8 @@ let rec intropattern_ids (loc,pat) = match pat with
   | IntroIdentifier id -> [id]
   | IntroOrAndPattern ll -> 
       List.flatten (List.map intropattern_ids (List.flatten ll))
-  | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ -> []
+  | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ 
+  | IntroForthcoming _ -> []
 
 let rec extract_ids ids = function
   | (id,VIntroPattern ipat)::tl when not (List.mem id ids) ->
@@ -1661,7 +1662,7 @@ let rec interp_intro_pattern ist gl = function
       loc, interp_intro_pattern_var loc ist (pf_env gl) id
   | loc, IntroFresh id ->
       loc, IntroFresh (interp_fresh_ident ist gl id)
-  | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _)
+  | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _ | IntroForthcoming _)
       as x -> x
 
 and interp_or_and_intro_pattern ist gl =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c3c1c4505..0452a9ed8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -432,30 +432,27 @@ let build_intro_tac id = function
   | MoveToEnd true -> introduction id
   | dest -> tclTHEN (introduction id) (move_hyp true id dest)
 
-let rec intro_gen loc name_flag move_flag force_flag gl =
+let rec intro_gen loc name_flag move_flag force_flag dep_flag gl =
   match kind_of_term (pf_concl gl) with
-    | Prod (name,t,_) -> 
+    | Prod (name,t,u) when not dep_flag or (dependent (mkRel 1) u) ->
 	build_intro_tac (find_name loc (name,None,t) gl name_flag) move_flag gl
-    | LetIn (name,b,t,_) ->
+    | LetIn (name,b,t,u) when not dep_flag or (dependent (mkRel 1) u) ->
 	build_intro_tac (find_name loc (name,Some b,t) gl name_flag) move_flag
 	  gl
     | _ -> 
 	if not force_flag then raise (RefinerError IntroNeedsProduct);
 	try
 	  tclTHEN try_red_in_concl
-	    (intro_gen loc name_flag move_flag force_flag) gl
+	    (intro_gen loc name_flag move_flag force_flag dep_flag) gl
 	with Redelimination ->
 	  user_err_loc(loc,"Intro",str "No product even after head-reduction.")
 
-let intro_mustbe_force id = intro_gen dloc (IntroMustBe id) no_move true
-let intro_using id = intro_gen dloc (IntroBasedOn (id,[])) no_move false
-let intro_force force_flag = intro_gen dloc (IntroAvoid []) no_move force_flag
-let intro = intro_force false
-let introf = intro_force true
-
-let intro_avoiding l = intro_gen dloc (IntroAvoid l) no_move false 
-
-let introf_move_name destopt = intro_gen dloc (IntroAvoid []) destopt true
+let intro_mustbe_force id = intro_gen dloc (IntroMustBe id) no_move true false
+let intro_using id = intro_gen dloc (IntroBasedOn (id,[])) no_move false false
+let intro = intro_gen dloc (IntroAvoid []) no_move false false
+let introf = intro_gen dloc (IntroAvoid []) no_move true false
+let intro_avoiding l = intro_gen dloc (IntroAvoid l) no_move false false
+let introf_move_name destopt = intro_gen dloc (IntroAvoid []) destopt true false
 
 (**** Multiple introduction tactics ****)
 
@@ -463,10 +460,13 @@ let rec intros_using = function
   | []     -> tclIDTAC
   | str::l -> tclTHEN (intro_using str) (intros_using l)
 
-let intros = tclREPEAT (intro_force false)
+let intros = tclREPEAT intro
 
 let intro_erasing id = tclTHEN (thin [id]) (introduction id)
 
+let intro_forthcoming_gen loc name_flag move_flag dep_flag =
+    tclREPEAT (intro_gen loc name_flag  move_flag false dep_flag)
+
 let rec get_next_hyp_position id = function
   | [] -> error ("No such hypothesis: " ^ string_of_id id)
   | (hyp,_,_) :: right ->
@@ -508,8 +508,8 @@ let intros_replacing ids gl =
 (* User-level introduction tactics *)
 
 let intro_move idopt hto = match idopt with
-  | None -> intro_gen dloc (IntroAvoid []) hto true
-  | Some id -> intro_gen dloc (IntroMustBe id) hto true
+  | None -> intro_gen dloc (IntroAvoid []) hto true false
+  | Some id -> intro_gen dloc (IntroMustBe id) hto true false
 
 let pf_lookup_hypothesis_as_renamed env ccl = function
   | AnonHyp n -> pf_lookup_index_as_renamed env ccl n
@@ -567,7 +567,7 @@ let try_intros_until tac = function
 let rec intros_move = function
   | [] -> tclIDTAC
   | (hyp,destopt) :: rest ->
-      tclTHEN (intro_gen dloc (IntroMustBe hyp) destopt false)
+      tclTHEN (intro_gen dloc (IntroMustBe hyp) destopt false false)
 	(intros_move rest)
 
 let dependent_in_decl a (_,c,t) =
@@ -1243,8 +1243,8 @@ let rewrite_hyp l2r id gl =
 let rec explicit_intro_names = function
 | (_, IntroIdentifier id) :: l ->
     id :: explicit_intro_names l
-| (_, (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _)) :: l ->
-    explicit_intro_names l
+| (_, (IntroWildcard | IntroAnonymous | IntroFresh _ 
+      | IntroRewrite _ | IntroForthcoming _)) :: l -> explicit_intro_names l
 | (_, IntroOrAndPattern ll) :: l' -> 
     List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll)
 | [] ->
@@ -1257,24 +1257,30 @@ let rec explicit_intro_names = function
 let rec intros_patterns b avoid thin destopt = function
   | (loc, IntroWildcard) :: l ->
       tclTHEN 
-        (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true)
+        (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l))
+	  no_move true false)
         (onLastHypId (fun id ->
 	  tclORELSE
 	    (tclTHEN (clear [id]) (intros_patterns b avoid thin destopt l))
 	    (intros_patterns b avoid ((loc,id)::thin) destopt l)))
   | (loc, IntroIdentifier id) :: l ->
       tclTHEN
-        (intro_gen loc (IntroMustBe id) destopt true)
+        (intro_gen loc (IntroMustBe id) destopt true false)
         (intros_patterns b avoid thin destopt l)
   | (loc, IntroAnonymous) :: l ->
       tclTHEN
         (intro_gen loc (IntroAvoid (avoid@explicit_intro_names l))
-	  destopt true)
+	  destopt true false)
         (intros_patterns b avoid thin destopt l)
   | (loc, IntroFresh id) :: l ->
       tclTHEN
         (intro_gen loc (IntroBasedOn (id, avoid@explicit_intro_names l))
-	  destopt true)
+	  destopt true false)
+        (intros_patterns b avoid thin destopt l)
+  | (loc, IntroForthcoming onlydeps) :: l ->
+      tclTHEN
+        (intro_forthcoming_gen loc (IntroAvoid (avoid@explicit_intro_names l))
+	  destopt onlydeps)
         (intros_patterns b avoid thin destopt l)
   | (loc, IntroOrAndPattern ll) :: l' ->
       tclTHEN
@@ -1284,7 +1290,8 @@ let rec intros_patterns b avoid thin destopt = function
 	    (intros_patterns b avoid thin destopt)))
   | (loc, IntroRewrite l2r) :: l ->
       tclTHEN 
-        (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true)
+        (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l))
+	  no_move true false)
         (onLastHypId (fun id ->
 	  tclTHEN
 	    (rewrite_hyp l2r id)
@@ -1319,6 +1326,8 @@ let prepare_intros s ipat gl = match ipat with
       onLastHypId
 	(intro_or_and_pattern loc true ll [] 
 	  (intros_patterns true [] [] no_move))
+  | IntroForthcoming _ -> user_err_loc
+      (loc,"",str "Introduction pattern for one hypothesis expected")
 
 let ipat_of_name = function
   | Anonymous -> None
@@ -1351,7 +1360,8 @@ let as_tac id ipat = match ipat with
       intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move)
         id
   | Some (loc,
-      (IntroIdentifier _ | IntroAnonymous | IntroFresh _ | IntroWildcard)) ->
+      (IntroIdentifier _ | IntroAnonymous | IntroFresh _ | 
+       IntroWildcard | IntroForthcoming _)) ->
       user_err_loc (loc,"", str "Disjunctive/conjunctive pattern expected")
   | None -> tclIDTAC
 
@@ -1587,13 +1597,13 @@ let letin_tac_gen with_eq name c ty occs gl =
       let refl = applist (eqdata.refl, [t;mkVar id]) in
       mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)),
       tclTHEN
-	(intro_gen loc (IntroMustBe heq) lastlhyp true)
+	(intro_gen loc (IntroMustBe heq) lastlhyp true false)
 	(thin_body [heq;id])
     | None ->
 	mkNamedLetIn id c t ccl, tclIDTAC in
   tclTHENLIST
     [ convert_concl_no_check newcl DEFAULTcast;
-      intro_gen dloc (IntroMustBe id) lastlhyp true;
+      intro_gen dloc (IntroMustBe id) lastlhyp true false;
       eq_tac;
       tclMAP convert_hyp_no_check depdecls ] gl
 
@@ -1691,13 +1701,18 @@ let rec first_name_buggy avoid gl (loc,pat) = match pat with
   | IntroWildcard -> no_move
   | IntroRewrite _ -> no_move
   | IntroIdentifier id -> MoveAfter id
-  | IntroAnonymous | IntroFresh _ -> (* buggy *) no_move
+  | IntroAnonymous | IntroFresh _ | IntroForthcoming _ -> (* buggy *) no_move
 
-let consume_pattern avoid id gl = function
+let rec consume_pattern avoid id isdep gl = function
   | [] -> ((dloc, IntroIdentifier (fresh_id avoid id gl)), [])
   | (loc,IntroAnonymous)::names ->
       let avoid = avoid@explicit_intro_names names in
       ((loc,IntroIdentifier (fresh_id avoid id gl)), names)
+  | (loc,IntroForthcoming true)::names when not isdep ->
+      consume_pattern avoid id isdep gl names
+  | (loc,IntroForthcoming _)::names as fullpat ->
+      let avoid = avoid@explicit_intro_names names in
+      ((loc,IntroIdentifier (fresh_id avoid id gl)), fullpat)
   | (loc,IntroFresh id')::names ->
       let avoid = avoid@explicit_intro_names names in
       ((loc,IntroIdentifier (fresh_id avoid id' gl)), names)
@@ -1719,14 +1734,14 @@ let induct_discharge statuslists destopt avoid' (avoid,ra) names gl =
   let avoid = avoid @ avoid' in
   let rec peel_tac ra names tophyp gl =
     match ra with
-    | (RecArg,recvarname) ::
-        (IndArg,hyprecname) :: ra' ->
+    | (RecArg,deprec,recvarname) ::
+        (IndArg,depind,hyprecname) :: ra' ->
         let recpat,names = match names with
           | [loc,IntroIdentifier id as pat] ->
               let id' = next_ident_away (add_prefix "IH" id) avoid in
 	      (pat, [dloc, IntroIdentifier id'])
-          | _ -> consume_pattern avoid recvarname gl names in
-        let hyprec,names = consume_pattern avoid hyprecname gl names in
+          | _ -> consume_pattern avoid recvarname deprec gl names in
+        let hyprec,names = consume_pattern avoid hyprecname depind gl names in
         (* IH stays at top: we need to update tophyp *)
         (* This is buggy for intro-or-patterns with different first hypnames *)
         (* Would need to pass peel_tac as a continuation of intros_patterns *)
@@ -1738,16 +1753,16 @@ let induct_discharge statuslists destopt avoid' (avoid,ra) names gl =
 	  [ intros_patterns true avoid [] (update destopt tophyp) [recpat];
 	    intros_patterns true avoid [] no_move [hyprec];
 	    peel_tac ra' names newtophyp] gl
-    | (IndArg,hyprecname) :: ra' ->
+    | (IndArg,dep,hyprecname) :: ra' ->
 	(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
-        let pat,names = consume_pattern avoid hyprecname gl names in
+        let pat,names = consume_pattern avoid hyprecname dep gl names in
 	tclTHEN (intros_patterns true avoid [] (update destopt tophyp) [pat])
           (peel_tac ra' names tophyp) gl
-    | (RecArg,recvarname) :: ra' ->
-        let pat,names = consume_pattern avoid recvarname gl names in
+    | (RecArg,dep,recvarname) :: ra' ->
+        let pat,names = consume_pattern avoid recvarname dep gl names in
 	tclTHEN (intros_patterns true avoid [] (update destopt tophyp) [pat]) 
           (peel_tac ra' names tophyp) gl
-    | (OtherArg,_) :: ra' ->
+    | (OtherArg,_,_) :: ra' ->
         let pat,names = match names with
           | [] -> (dloc, IntroAnonymous), []
           | pat::names -> pat,names in
@@ -2477,8 +2492,10 @@ let compute_elim_signature elimc elimt names_info ind_type_guess =
 	    | _ -> OtherArg in 
 	let rec check_branch p c = 
 	  match kind_of_term c with
-	    | Prod (_,t,c) -> is_pred p t :: check_branch (p+1) c
-	    | LetIn (_,_,_,c) -> OtherArg :: check_branch (p+1) c
+	    | Prod (_,t,c) ->
+		(is_pred p t, dependent (mkRel 1) c) :: check_branch (p+1) c
+	    | LetIn (_,_,_,c) ->
+		(OtherArg, dependent (mkRel 1) c) :: check_branch (p+1) c
 	    | _ when is_pred p c = IndArg -> []
 	    | _ -> raise Exit in 
 	let rec find_branches p lbrch = 
@@ -2487,11 +2504,12 @@ let compute_elim_signature elimc elimt names_info ind_type_guess =
 		(try
 		  let lchck_brch = check_branch p t in
 		  let n = List.fold_left 
-		    (fun n b -> if b=RecArg then n+1 else n) 0 lchck_brch in
+		    (fun n (b,_) -> if b=RecArg then n+1 else n) 0 lchck_brch in
 		  let recvarname, hyprecname, avoid = 
 		    make_up_names n scheme.indref names_info in
 		  let namesign = 
-		    List.map (fun b -> (b,if b=IndArg then hyprecname else recvarname))
+		    List.map (fun (b,dep) ->
+		      (b,dep,if b=IndArg then hyprecname else recvarname))
 		      lchck_brch in
 		  (avoid,namesign) :: find_branches (p+1) brs
 		with Exit-> error_ind_scheme "the branches of")
@@ -2508,8 +2526,10 @@ let compute_elim_signature elimc elimt names_info ind_type_guess =
 	    | _ when hd = indhd -> RecArg
 	    | _ -> OtherArg in
 	let rec check_branch p c = match kind_of_term c with
-	  | Prod (_,t,c) -> is_pred p t :: check_branch (p+1) c
-	  | LetIn (_,_,_,c) -> OtherArg :: check_branch (p+1) c
+	  | Prod (_,t,c) -> 
+	      (is_pred p t, dependent (mkRel 1) c) :: check_branch (p+1) c
+	  | LetIn (_,_,_,c) ->
+	      (OtherArg, dependent (mkRel 1) c) :: check_branch (p+1) c
 	  | _ when is_pred p c = IndArg -> []
 	  | _ -> raise Exit in 
 	let rec find_branches p lbrch =
@@ -2518,11 +2538,12 @@ let compute_elim_signature elimc elimt names_info ind_type_guess =
 		(try
 		  let lchck_brch = check_branch p t in
 		  let n = List.fold_left 
-		    (fun n b -> if b=RecArg then n+1 else n) 0 lchck_brch in
+		    (fun n (b,_) -> if b=RecArg then n+1 else n) 0 lchck_brch in
 		  let recvarname, hyprecname, avoid = 
 		    make_up_names n scheme.indref names_info in
 		  let namesign = 
-		    List.map (fun b -> (b,if b=IndArg then hyprecname else recvarname))
+		    List.map (fun (b,dep) -> 
+		      (b,dep,if b=IndArg then hyprecname else recvarname))
 		      lchck_brch in
 		  (avoid,namesign) :: find_branches (p+1) brs
 		with Exit -> error_ind_scheme "the branches of")
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index e00088dd8..136833ad7 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -65,7 +65,6 @@ val find_intro_names : rel_context -> goal sigma -> identifier list
 
 val intro                : tactic
 val introf               : tactic
-val intro_force          : bool -> tactic
 val intro_move        : identifier option -> identifier move_location -> tactic
 
   (* [intro_avoiding idl] acts as intro but prevents the new identifier
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 *)
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index d1f93d498..f024339d8 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -15,18 +15,27 @@ Require Import Zorder.
 Require Import Zcompare.
 Open Local Scope Z_scope.
 
+(* begin hide *)
+(* Trivial, to deprecate? *)
 Lemma Dcompare_inf : forall r:comparison, {r = Eq} + {r = Lt} + {r = Gt}.
 Proof.
-  simple induction r; auto with arith. 
+  induction r; auto.
+Defined.
+(* end hide *)
+
+Lemma Zcompare_rect :
+  forall (P:Type) (n m:Z),
+    ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.
+Proof.
+  intros * H1 H2 H3.
+  destruct (n ?= m); auto. 
 Defined.
 
 Lemma Zcompare_rec :
   forall (P:Set) (n m:Z),
     ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.
 Proof.
-  intros P x y H1 H2 H3.
-  elim (Dcompare_inf (x ?= y)).
-  intro H. elim H; auto with arith. auto with arith.
+  intro; apply Zcompare_rect.
 Defined.
 
 Section decidability.
@@ -37,12 +46,7 @@ Section decidability.
 
   Definition Z_eq_dec : {x = y} + {x <> y}.
   Proof.
-    apply Zcompare_rec with (n := x) (m := y).
-    intro. left. elim (Zcompare_Eq_iff_eq x y); auto with arith.
-    intro H3. right. elim (Zcompare_Eq_iff_eq x y). intros H1 H2. unfold not in |- *. intro H4.
-    rewrite (H2 H4) in H3. discriminate H3.
-    intro H3. right. elim (Zcompare_Eq_iff_eq x y). intros H1 H2. unfold not in |- *. intro H4.
-    rewrite (H2 H4) in H3. discriminate H3.
+    decide equality; apply positive_eq_dec.
   Defined. 
 
   (** * Decidability of order on binary integers *)
@@ -214,13 +218,16 @@ Proof.
     [ right; assumption | left; apply (not_Zeq_inf _ _ H) ].
 Defined.
 
-
-
-Definition Z_zerop : forall x:Z, {x = 0} + {x <> 0}.
+(* begin hide *)
+(* To deprecate ? *)
+Corollary Z_zerop : forall x:Z, {x = 0} + {x <> 0}.
 Proof.
   exact (fun x:Z => Z_eq_dec x 0).
 Defined.
 
-Definition Z_notzerop (x:Z) := sumbool_not _ _ (Z_zerop x).
+Corollary Z_notzerop : forall (x:Z), {x <> 0} + {x = 0}.
+Proof (fun x => sumbool_not _ _ (Z_zerop x)).
 
-Definition Z_noteq_dec (x y:Z) := sumbool_not _ _ (Z_eq_dec x y).
+Corollary Z_noteq_dec : forall (x y:Z), {x <> y} + {x = y}.
+Proof (fun x y => sumbool_not _ _ (Z_eq_dec x y)).
+(* end hide *)