diff options
| author | Pierre-Marie Pédrot | 2017-09-05 15:59:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-05 16:17:23 +0200 |
| commit | c38e196fc175aaca2268f73107c9658c7af7d9fc (patch) | |
| tree | f5ff48a6fa0bc9b794819aa6c56355117f4a824a /theories | |
| parent | 2b0e0ad1062ad49c8bd7d4a7d183fe0119f81803 (diff) | |
Binding move and intro.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Notations.v | 5 | ||||
| -rw-r--r-- | theories/Std.v | 4 |
2 files changed, 9 insertions, 0 deletions
diff --git a/theories/Notations.v b/theories/Notations.v index 8a3e769d12..9ecca018af 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -399,6 +399,11 @@ Ltac2 exact0 ev c := Ltac2 Notation "exact" c(thunk(open_constr)) := exact0 false c. Ltac2 Notation "eexact" c(thunk(open_constr)) := exact0 true c. +Ltac2 Notation "intro" id(opt(ident)) mv(opt(move_location)) := Std.intro id mv. +Ltac2 Notation intro := intro. + +Ltac2 Notation "move" id(ident) mv(move_location) := Std.move id mv. + Ltac2 Notation reflexivity := Std.reflexivity (). Ltac2 symmetry0 cl := diff --git a/theories/Std.v b/theories/Std.v index 3f98bdbaab..a937560b10 100644 --- a/theories/Std.v +++ b/theories/Std.v @@ -214,6 +214,10 @@ Ltac2 @ external inversion : inversion_kind -> destruction_arg -> intro_pattern (** coretactics *) +Ltac2 @ external move : ident -> move_location -> unit := "ltac2" "tac_move". + +Ltac2 @ external intro : ident option -> move_location option -> unit := "ltac2" "tac_intro". + (** extratactics *) Ltac2 @ external discriminate : evar_flag -> destruction_arg option -> unit := "ltac2" "tac_discriminate". |