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 /theories | |
| parent | c96b746b17a37e242fc01103d22fa0b852da84c5 (diff) | |
Adding a few standard notations for Ltac1 tactics.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Ltac2.v | 1 | ||||
| -rw-r--r-- | theories/Notations.v | 37 |
2 files changed, 38 insertions, 0 deletions
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. |