summaryrefslogtreecommitdiff
path: root/theories/ZArith/Int.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /theories/ZArith/Int.v
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'theories/ZArith/Int.v')
-rw-r--r--theories/ZArith/Int.v47
1 files changed, 8 insertions, 39 deletions
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index 3cee9190..fcb44d6f 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -7,11 +7,11 @@
(***********************************************************************)
(* Finite sets library.
- * Authors: Pierre Letouzey and Jean-Christophe Filliâtre
- * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
+ * Authors: Pierre Letouzey and Jean-Christophe Filliâtre
+ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
* 91405 Orsay, France *)
-(* $Id: Int.v 9319 2006-10-30 12:41:21Z barras $ *)
+(* $Id: Int.v 10739 2008-04-01 14:45:20Z herbelin $ *)
(** An axiomatization of integers. *)
@@ -352,46 +352,15 @@ Module MoreInt (I:Int).
Ltac i2z_refl :=
i2z_gen;
match goal with |- ?t =>
- let e := p2ep t
- in
- (change (ep2p e);
- apply norm_ep_correct2;
- simpl)
+ let e := p2ep t in
+ change (ep2p e); apply norm_ep_correct2; simpl
end.
- Ltac iauto := i2z_refl; auto.
- Ltac iomega := i2z_refl; intros; romega.
-
- Open Scope Z_scope.
-
- Lemma max_spec : forall (x y:Z),
- x >= y /\ Zmax x y = x \/
- x < y /\ Zmax x y = y.
- Proof.
- intros; unfold Zmax, Zlt, Zge.
- destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate.
- Qed.
-
- Ltac omega_max_genspec x y :=
- generalize (max_spec x y);
- (let z := fresh "z" in let Hz := fresh "Hz" in
- set (z:=Zmax x y); clearbody z).
-
- Ltac omega_max_loop :=
- match goal with
- (* hack: we don't want [i2z (height ...)] to be reduced by romega later... *)
- | |- context [ i2z (?f ?x) ] =>
- let i := fresh "i2z" in (set (i:=i2z (f x)); clearbody i); omega_max_loop
- | |- context [ Zmax ?x ?y ] => omega_max_genspec x y; omega_max_loop
- | _ => intros
- end.
-
- Ltac omega_max := i2z_refl; omega_max_loop; try romega.
+ (* i2z_refl can be replaced below by (simpl in *; i2z).
+ The reflexive version improves compilation of AVL files by about 15% *)
- Ltac false_omega := i2z_refl; intros; romega.
- Ltac false_omega_max := elimtype False; omega_max.
+ Ltac omega_max := i2z_refl; romega with Z.
- Open Scope Int_scope.
End MoreInt.