diff options
Diffstat (limited to 'test-suite/ltac2')
| -rw-r--r-- | test-suite/ltac2/notations.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/ltac2/notations.v b/test-suite/ltac2/notations.v index 3d2a875e38..32c8a7cbe7 100644 --- a/test-suite/ltac2/notations.v +++ b/test-suite/ltac2/notations.v @@ -1,6 +1,8 @@ From Ltac2 Require Import Ltac2. From Coq Require Import ZArith String List. +(** * Test cases for the notation system itself *) + Open Scope Z_scope. Check 1 + 1 : Z. @@ -22,3 +24,9 @@ Lemma maybe : list bool. Proof. refine (sl ["left" =? "right"]). Qed. + +(** * Test cases for specific notations with special contexts *) + +(** ** Test eval ... in / reduction tactics *) + +(** Moved to test-suite/output/ltac2_notations_eval_in.v so that the output can be checked s*) |