diff options
| -rw-r--r-- | tests/example2.v | 8 | ||||
| -rw-r--r-- | theories/Notations.v | 3 |
2 files changed, 11 insertions, 0 deletions
diff --git a/tests/example2.v b/tests/example2.v index af664ef163..6b26b78022 100644 --- a/tests/example2.v +++ b/tests/example2.v @@ -182,3 +182,11 @@ Proof. lazy. reflexivity. Qed. + +Goal let x := 1 + 1 - 1 in x = x. +Proof. +intros x. +unfold &x at 1. +let x := reference:(Nat.sub) in unfold Nat.add, $x in x. +reflexivity. +Qed. diff --git a/theories/Notations.v b/theories/Notations.v index 26d40fcb89..62d5d65d7c 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -273,6 +273,9 @@ Ltac2 Notation "lazy" s(strategy) cl(opt(clause)) := Std.lazy s (default_on_concl cl). Ltac2 Notation lazy := lazy. +Ltac2 Notation "unfold" pl(list1(seq(reference, occurrences), ",")) cl(opt(clause)) := + Std.unfold pl (default_on_concl cl). + Ltac2 fold0 pl cl := let cl := default_on_concl cl in Control.enter (fun () => Control.with_holes pl (fun pl => Std.fold pl cl)). |