diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ltac2/notations.v | 24 | ||||
| -rw-r--r-- | test-suite/success/goal_selector.v | 8 |
2 files changed, 29 insertions, 3 deletions
diff --git a/test-suite/ltac2/notations.v b/test-suite/ltac2/notations.v new file mode 100644 index 0000000000..3d2a875e38 --- /dev/null +++ b/test-suite/ltac2/notations.v @@ -0,0 +1,24 @@ +From Ltac2 Require Import Ltac2. +From Coq Require Import ZArith String List. + +Open Scope Z_scope. + +Check 1 + 1 : Z. + +Ltac2 Notation "ex" arg(constr(nat,Z)) := arg. + +Check (1 + 1)%nat%Z = 1%nat. + +Lemma two : nat. + refine (ex (1 + 1)). +Qed. + +Import ListNotations. +Close Scope list_scope. + +Ltac2 Notation "sl" arg(constr(string,list)) := arg. + +Lemma maybe : list bool. +Proof. + refine (sl ["left" =? "right"]). +Qed. diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v index 0951c5c8d4..ae834e7696 100644 --- a/test-suite/success/goal_selector.v +++ b/test-suite/success/goal_selector.v @@ -13,13 +13,15 @@ Goal two false /\ two true /\ two false /\ two true /\ two true /\ two true. Proof. do 2 dup. - repeat split. - 2, 4-99, 100-3:idtac. + Fail 7:idtac. + Fail 2-1:idtac. + 1,2,4-6:idtac. 2-5:exact One. par:exact Zero. - repeat split. 3-6:swap 1 4. 1-5:swap 1 5. - 0-4:exact One. + 1-4:exact One. all:exact Zero. - repeat split. 1, 3:exact Zero. @@ -34,7 +36,7 @@ Qed. Goal True -> True. Proof. - intros y; only 1-2 : repeat idtac. + intros y. 1-1:match goal with y : _ |- _ => let x := y in idtac x end. Fail 1-1:let x := y in idtac x. 1:let x := y in idtac x. |