diff options
| -rw-r--r-- | tests/example2.v | 25 | ||||
| -rw-r--r-- | theories/Notations.v | 28 |
2 files changed, 47 insertions, 6 deletions
diff --git a/tests/example2.v b/tests/example2.v index 1856663953..af664ef163 100644 --- a/tests/example2.v +++ b/tests/example2.v @@ -157,3 +157,28 @@ intros H. split; fold (1 + 0) (1 + 0) in H. reflexivity. Qed. + +Goal 1 + 1 = 2. +Proof. +cbv [ Nat.add ]. +reflexivity. +Qed. + +Goal 1 + 1 = 2. +Proof. +let x := reference:(Nat.add) in +cbn beta iota delta [ $x ]. +reflexivity. +Qed. + +Goal 1 + 1 = 2. +Proof. +simpl beta. +reflexivity. +Qed. + +Goal 1 + 1 = 2. +Proof. +lazy. +reflexivity. +Qed. diff --git a/theories/Notations.v b/theories/Notations.v index 8c2c09a2b5..26d40fcb89 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -257,13 +257,21 @@ 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 "simpl" s(strategy) pl(opt(seq(pattern, occurrences))) cl(opt(clause)) := + Std.simpl s pl (default_on_concl cl). +Ltac2 Notation simpl := simpl. -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 Notation "cbv" s(strategy) cl(opt(clause)) := + Std.cbv s (default_on_concl cl). +Ltac2 Notation cbv := cbv. + +Ltac2 Notation "cbn" s(strategy) cl(opt(clause)) := + Std.cbn s (default_on_concl cl). +Ltac2 Notation cbn := cbn. + +Ltac2 Notation "lazy" s(strategy) cl(opt(clause)) := + Std.lazy s (default_on_concl cl). +Ltac2 Notation lazy := lazy. Ltac2 fold0 pl cl := let cl := default_on_concl cl in @@ -275,6 +283,14 @@ Ltac2 Notation "fold" pl(thunk(list1(open_constr))) cl(opt(clause)) := Ltac2 Notation "pattern" pl(list1(seq(constr, occurrences), ",")) cl(opt(clause)) := Std.pattern pl (default_on_concl cl). +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 rewrite0 ev rw cl tac := let tac := match tac with | None => None |