diff options
| author | Pierre-Marie Pédrot | 2020-04-10 13:12:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-10 13:12:49 +0200 |
| commit | f373d82ffa7d30df6ace77f7064d4eed6f321b90 (patch) | |
| tree | 52f34212ef28f20d52ff7558e74391cae7ed8dfb /theories/FSets | |
| parent | 4a3f3bb73bce337137a9deba3d67115a8400a74a (diff) | |
| parent | aa889ee516453af65bd74ffedf8ec3761f97eb43 (diff) | |
Merge PR #11882: Adding a short form of Ltac2 Fresh.fresh
Reviewed-by: MSoegtropIMC
Reviewed-by: ppedrot
Ack-by: tchajed
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 82055c4752..f78c0ecc1e 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -550,14 +550,14 @@ Ltac intuition_in := repeat (intuition; inv In; inv MapsTo). Let's do its job by hand: *) Ltac join_tac := - intros l; induction l as [| ll _ lx ld lr Hlr lh]; - [ | intros x d r; induction r as [| rl Hrl rx rd rr _ rh]; unfold join; - [ | destruct (gt_le_dec lh (rh+2)) as [GT|LE]; + intros ?l; induction l as [| ?ll _ ?lx ?ld ?lr ?Hlr ?lh]; + [ | intros ?x ?d ?r; induction r as [| ?rl ?Hrl ?rx ?rd ?rr _ ?rh]; unfold join; + [ | destruct (gt_le_dec lh (rh+2)) as [?GT|?LE]; [ match goal with |- context [ bal ?u ?v ?w ?z ] => replace (bal u v w z) with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto] end - | destruct (gt_le_dec rh (lh+2)) as [GT'|LE']; + | destruct (gt_le_dec rh (lh+2)) as [?GT'|?LE']; [ match goal with |- context [ bal ?u ?v ?w ?z ] => replace (bal u v w z) with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto] |