diff options
| -rw-r--r-- | tests/example2.v | 34 | ||||
| -rw-r--r-- | theories/Notations.v | 18 |
2 files changed, 52 insertions, 0 deletions
diff --git a/tests/example2.v b/tests/example2.v index bfb1b07e7a..1856663953 100644 --- a/tests/example2.v +++ b/tests/example2.v @@ -123,3 +123,37 @@ intros n r. hnf in r. split. Qed. + +Goal 1 = 0 -> 0 = 0. +Proof. +intros H. +pattern 0 at 1. +let occ := 2 in pattern 1 at 1, 0 at $occ in H. +reflexivity. +Qed. + +Goal 1 + 1 = 2. +Proof. +vm_compute. +reflexivity. +Qed. + +Goal 1 + 1 = 2. +Proof. +native_compute. +reflexivity. +Qed. + +Goal 1 + 1 = 2 - 0 -> True. +Proof. +intros H. +vm_compute plus in H. +reflexivity. +Qed. + +Goal 1 = 0 -> True /\ True. +Proof. +intros H. +split; fold (1 + 0) (1 + 0) in H. +reflexivity. +Qed. diff --git a/theories/Notations.v b/theories/Notations.v index 910b6d5463..8c2c09a2b5 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -257,6 +257,24 @@ Ltac2 Notation "hnf" cl(opt(clause)) := Std.hnf (default_on_concl cl). Ltac2 Notation hnf := hnf. +Ltac2 Notation "vm_compute" pl(opt(seq(pattern, occurrences))) cl(opt(clause)) := + Std.vm pl (default_on_concl cl). +Ltac2 Notation vm_compute := vm_compute. + +Ltac2 Notation "native_compute" pl(opt(seq(pattern, occurrences))) cl(opt(clause)) := + Std.native pl (default_on_concl cl). +Ltac2 Notation native_compute := native_compute. + +Ltac2 fold0 pl cl := + let cl := default_on_concl cl in + Control.enter (fun () => Control.with_holes pl (fun pl => Std.fold pl cl)). + +Ltac2 Notation "fold" pl(thunk(list1(open_constr))) cl(opt(clause)) := + fold0 pl cl. + +Ltac2 Notation "pattern" pl(list1(seq(constr, occurrences), ",")) cl(opt(clause)) := + Std.pattern pl (default_on_concl cl). + Ltac2 rewrite0 ev rw cl tac := let tac := match tac with | None => None |