diff options
| author | Michael Soegtrop | 2020-04-01 16:38:17 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2020-05-17 09:43:42 +0200 |
| commit | e6b295a62a82df6fa92b559bb3ce079d5fa42240 (patch) | |
| tree | 3e029fc5c501e51feba8b4637c542e025f4de708 /test-suite/ltac2 | |
| parent | d81bb4085ccad294cb1edd59ed5e0f9fd4d3b23a (diff) | |
Ltac2: add notations for eval cbv in ... and other in place reductions
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*) |