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 /theories | |
| parent | 60a98c8092a0293b852712f8e21ead6e0ef1e064 (diff) | |
Adding a notation for the unfold tactic.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Notations.v | 3 |
1 files changed, 3 insertions, 0 deletions
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)). |