From 53374f189cc9b9b67ff94d5362fdffdba6c779a3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 2 Aug 2017 01:42:14 +0200
Subject: Adding a few standard notations for Ltac1 tactics.

---
 tests/example2.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests')

diff --git a/tests/example2.v b/tests/example2.v
index ffdb723ffb..398f33561e 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -1,6 +1,6 @@
 Require Import Ltac2.Ltac2.
 
-Ltac2 Notation "split" bnd(bindings) := Std.split bnd.
+Import Ltac2.Notations.
 
 Goal exists n, n = 0.
 Proof.
-- 
cgit v1.2.3