From 29e7f5e8aba98c8d9dbdb8ca64fd8aed5b705d38 Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 28 Mar 2009 18:16:22 +0000 Subject: ZArith/Int: no need to load romega here (but rather in FullAVL) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12027 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/Int.v | 23 ++++++++++------------- 1 file changed, 10 insertions(+), 13 deletions(-) (limited to 'theories/ZArith') diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 562000d8f..24d2696c5 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -22,7 +22,6 @@ *) Require Import ZArith. -Require Import ROmega. Delimit Scope Int_scope with I. @@ -135,23 +134,23 @@ Module MoreInt (I:Int). | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); i2z_gen | H : (eq (A:=int) ?a ?b) |- _ => generalize (f_equal i2z H); clear H; i2z_gen - | H : (eq (A:=Z) ?a ?b) |- _ => generalize H; clear H; i2z_gen - | H : (Zlt ?a ?b) |- _ => generalize H; clear H; i2z_gen - | H : (Zle ?a ?b) |- _ => generalize H; clear H; i2z_gen - | H : (Zgt ?a ?b) |- _ => generalize H; clear H; i2z_gen - | H : (Zge ?a ?b) |- _ => generalize H; clear H; i2z_gen + | H : (eq (A:=Z) ?a ?b) |- _ => revert H; i2z_gen + | H : (Zlt ?a ?b) |- _ => revert H; i2z_gen + | H : (Zle ?a ?b) |- _ => revert H; i2z_gen + | H : (Zgt ?a ?b) |- _ => revert H; i2z_gen + | H : (Zge ?a ?b) |- _ => revert H; i2z_gen | H : _ -> ?X |- _ => (* A [Set] or [Type] part cannot be dealt with easily using the [ExprP] datatype. So we forget it, leaving a goal that can be weaker than the original. *) match type of X with | Type => clear H; i2z_gen - | Prop => generalize H; clear H; i2z_gen + | Prop => revert H; i2z_gen end - | H : _ <-> _ |- _ => generalize H; clear H; i2z_gen - | H : _ /\ _ |- _ => generalize H; clear H; i2z_gen - | H : _ \/ _ |- _ => generalize H; clear H; i2z_gen - | H : ~ _ |- _ => generalize H; clear H; i2z_gen + | H : _ <-> _ |- _ => revert H; i2z_gen + | H : _ /\ _ |- _ => revert H; i2z_gen + | H : _ \/ _ |- _ => revert H; i2z_gen + | H : ~ _ |- _ => revert H; i2z_gen | _ => idtac end. @@ -358,8 +357,6 @@ Module MoreInt (I:Int). (* i2z_refl can be replaced below by (simpl in *; i2z). The reflexive version improves compilation of AVL files by about 15% *) - - Ltac omega_max := i2z_refl; romega with Z. End MoreInt. -- cgit v1.2.3