diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | tests/example2.v | 2 | ||||
| -rw-r--r-- | theories/Ltac2.v | 1 | ||||
| -rw-r--r-- | theories/Notations.v | 37 |
4 files changed, 40 insertions, 1 deletions
diff --git a/_CoqProject b/_CoqProject index b8064c46a4..583639612b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -35,4 +35,5 @@ theories/Message.v theories/Constr.v theories/Pattern.v theories/Std.v +theories/Notations.v theories/Ltac2.v 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. diff --git a/theories/Ltac2.v b/theories/Ltac2.v index 9aaee850cd..07229797da 100644 --- a/theories/Ltac2.v +++ b/theories/Ltac2.v @@ -17,3 +17,4 @@ Require Ltac2.Constr. Require Ltac2.Control. Require Ltac2.Pattern. Require Ltac2.Std. +Require Ltac2.Notations. diff --git a/theories/Notations.v b/theories/Notations.v new file mode 100644 index 0000000000..d0400667db --- /dev/null +++ b/theories/Notations.v @@ -0,0 +1,37 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Ltac2.Init. +Require Ltac2.Control Ltac2.Std. + +Ltac2 Notation "intros" p(intropatterns) := Std.intros p. + +Ltac2 Notation "eintros" p(intropatterns) := Std.eintros p. + +Ltac2 Notation "split" bnd(thunk(bindings)) := + Control.with_holes bnd (fun bnd => Std.split bnd). + +Ltac2 Notation "esplit" bnd(bindings) := Std.esplit bnd. + +Ltac2 Notation "left" bnd(thunk(bindings)) := + Control.with_holes bnd (fun bnd => Std.left bnd). + +Ltac2 Notation "eleft" bnd(bindings) := Std.eleft bnd. + +Ltac2 Notation "right" bnd(thunk(bindings)) := + Control.with_holes bnd (fun bnd => Std.right bnd). + +Ltac2 Notation "eright" bnd(bindings) := Std.eright bnd. + +Ltac2 Notation "constructor" := Std.constructor (). +Ltac2 Notation "constructor" n(tactic) bnd(thunk(bindings)) := + Control.with_holes bnd (fun bnd => Std.constructor_n n bnd). + +Ltac2 Notation "econstructor" := Std.econstructor (). +Ltac2 Notation "econstructor" n(tactic) bnd(bindings) := + Std.econstructor_n n bnd. |