From d2bd5d87d23d443f6e41496bdfe5f8e82d675634 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:59 +0000 Subject: Modularization of BinInt, related fixes in the stdlib All the functions about Z is now in a separated file BinIntDef, which is Included in BinInt.Z. This BinInt.Z directly implements ZAxiomsSig, and instantiates derived properties ZProp. Note that we refer to Z instead of t inside BinInt.Z, otherwise ring breaks later on @eq Z.t git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14106 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/MSets/MSetAVL.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/MSets') diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index db6616b34..1e2ddb7a6 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -876,12 +876,12 @@ Open Scope Int_scope. Ltac join_tac := intro l; induction l as [| ll _ lx lr Hlr lh]; [ | intros x r; induction r as [| rl Hrl rx rr _ rh]; unfold join; - [ | destruct (gt_le_dec lh (rh+2)); + [ | destruct (gt_le_dec lh (rh+2)) as [GT|LE]; [ match goal with |- context b [ bal ?a ?b ?c] => replace (bal a b c) with (bal ll lx (join lr x (Node rl rx rr rh))); [ | auto] end - | destruct (gt_le_dec rh (lh+2)); + | destruct (gt_le_dec rh (lh+2)) as [GT'|LE']; [ match goal with |- context b [ bal ?a ?b ?c] => replace (bal a b c) with (bal (join (Node ll lx lr lh) x rl) rx rr); [ | auto] @@ -904,7 +904,7 @@ Instance join_ok : forall l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r), Ok (join l x r). Proof. join_tac; auto with *; inv; apply bal_ok; auto; - clear Hrl Hlr z; intro; intros; rewrite join_spec in *. + clear Hrl Hlr; intro; intros; rewrite join_spec in *. intuition; [ setoid_replace y with x | ]; eauto. intuition; [ setoid_replace y with x | ]; eauto. Qed. -- cgit v1.2.3