From e6b295a62a82df6fa92b559bb3ce079d5fa42240 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Wed, 1 Apr 2020 16:38:17 +0200
Subject: Ltac2: add notations for eval cbv in ... and other in place
 reductions

---
 test-suite/ltac2/notations.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'test-suite/ltac2')

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*)
-- 
cgit v1.2.3