diff options
| author | Hugo Herbelin | 2020-03-22 12:30:55 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-03 20:33:27 +0200 |
| commit | aa889ee516453af65bd74ffedf8ec3761f97eb43 (patch) | |
| tree | 9dbe0527c1fc7dd34eb8fa9a2462d3a96048baaa /theories/FSets | |
| parent | 9e98c1ebb9472f1c77eb0289bd64e525d58d99de (diff) | |
Avoiding using a fixed introduction name in Ltac code of stdlib.
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] |