diff options
| author | Pierre-Marie Pédrot | 2017-08-02 01:42:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-02 02:12:36 +0200 |
| commit | 53374f189cc9b9b67ff94d5362fdffdba6c779a3 (patch) | |
| tree | 8e90f7fa3646d65be369e6db5f0427c7a3b9d09d | |
| parent | c96b746b17a37e242fc01103d22fa0b852da84c5 (diff) | |
Adding a few standard notations for Ltac1 tactics.
| -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. |