diff options
| author | Jason Gross | 2020-05-17 16:08:54 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-05-17 16:08:54 -0400 |
| commit | 5ec400894c62d7f73caa3f554a5c9b9ee5b8f8d6 (patch) | |
| tree | 8c88f245ad0b4261f5faf7f8c91005365f6d273c /test-suite/ltac2 | |
| parent | b9591f15d75886456ff28984934de73d6a516af5 (diff) | |
| parent | e6b295a62a82df6fa92b559bb3ce079d5fa42240 (diff) | |
Merge PR #11981: Ltac2: add notations for eval cbv in ... and other in place reductions
Reviewed-by: JasonGross
Ack-by: Zimmi48
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*) |