diff options
| author | Pierre-Marie Pédrot | 2017-08-24 17:14:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-24 17:15:48 +0200 |
| commit | c515a8acb4acbe7e73121f1060ffef31d96a1436 (patch) | |
| tree | a99277a77c26e3cafa33556fbbecd916d4ec0fe3 | |
| parent | 60a98c8092a0293b852712f8e21ead6e0ef1e064 (diff) | |
Adding a notation for the unfold tactic.
| -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)). |