diff options
Diffstat (limited to 'theories/ssr')
| -rw-r--r-- | theories/ssr/ssreflect.v | 43 |
1 files changed, 16 insertions, 27 deletions
diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v index dc81b5cca7..db572d25d8 100644 --- a/theories/ssr/ssreflect.v +++ b/theories/ssr/ssreflect.v @@ -671,43 +671,32 @@ Module Export ipat. Notation "'[' 'apply' ']'" := (ltac:(let f := fresh "_top_" in move=> f {}/f)) (at level 0, only parsing) : ssripat_scope. -(** We try to preserve the naming by matching the names from the goal. - We do 'move' to perform a hnf before trying to match. **) +(* we try to preserve the naming by matching the names from the goal *) +(* we do move to perform a hnf before trying to match *) Notation "'[' 'swap' ']'" := (ltac:(move; - lazymatch goal with - | |- forall (x : _), _ => let x := fresh x in move=> x; move; - lazymatch goal with - | |- forall (y : _), _ => let y := fresh y in move=> y; move: y x - | |- let y := _ in _ => let y := fresh y in move=> y; move: @y x - | _ => let y := fresh "_top_" in move=> y; move: y x - end - | |- let x := _ in _ => let x := fresh x in move => x; move; - lazymatch goal with - | |- forall (y : _), _ => let y := fresh y in move=> y; move: y @x - | |- let y := _ in _ => let y := fresh y in move=> y; move: @y @x - | _ => let y := fresh "_top_" in move=> y; move: y x - end - | _ => let x := fresh "_top_" in let x := fresh x in move=> x; move; - lazymatch goal with - | |- forall (y : _), _ => let y := fresh y in move=> y; move: y @x - | |- let y := _ in _ => let y := fresh y in move=> y; move: @y @x - | _ => let y := fresh "_top_" in move=> y; move: y x - end - end)) + let x := lazymatch goal with + | |- forall (x : _), _ => fresh x | |- let x := _ in _ => fresh x | _ => fresh "_top_" + end in intro x; move; + let y := lazymatch goal with + | |- forall (y : _), _ => fresh y | |- let y := _ in _ => fresh y | _ => fresh "_top_" + end in intro y; revert x; revert y)) (at level 0, only parsing) : ssripat_scope. + +(* we try to preserve the naming by matching the names from the goal *) +(* we do move to perform a hnf before trying to match *) Notation "'[' 'dup' ']'" := (ltac:(move; lazymatch goal with | |- forall (x : _), _ => - let x := fresh x in move=> x; - let copy := fresh x in have copy := x; move: copy x + let x := fresh x in intro x; + let copy := fresh x in have copy := x; revert x; revert copy | |- let x := _ in _ => - let x := fresh x in move=> x; + let x := fresh x in intro x; let copy := fresh x in pose copy := x; - do [unfold x in (value of copy)]; move: @copy @x + do [unfold x in (value of copy)]; revert x; revert copy | |- _ => let x := fresh "_top_" in move=> x; - let copy := fresh "_top" in have copy := x; move: copy x + let copy := fresh "_top" in have copy := x; revert x; revert copy end)) (at level 0, only parsing) : ssripat_scope. |