diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Notations.v | 25 | ||||
| -rw-r--r-- | theories/Std.v | 2 |
2 files changed, 27 insertions, 0 deletions
diff --git a/theories/Notations.v b/theories/Notations.v index 20f01c3b48..4ce9fc0dbd 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -138,3 +138,28 @@ Ltac2 Notation "edestruct" ic(list1(induction_clause, ",")) use(thunk(opt(seq("using", constr, bindings)))) := destruct0 true ic use. + +Ltac2 rewrite0 ev rw cl tac := + let tac := match tac with + | None => None + | Some p => + let ((_, tac)) := p in + Some tac + end in + let cl := match cl with + | None => { Std.on_hyps := Some []; Std.on_concl := Std.AllOccurrences } + | Some cl => cl + end in + Std.rewrite ev rw cl tac. + +Ltac2 Notation "rewrite" + rw(list1(rewriting, ",")) + cl(opt(clause)) + tac(opt(seq("by", thunk(tactic)))) := + rewrite0 false rw cl tac. + +Ltac2 Notation "erewrite" + rw(list1(rewriting, ",")) + cl(opt(clause)) + tac(opt(seq("by", thunk(tactic)))) := + rewrite0 true rw cl tac. diff --git a/theories/Std.v b/theories/Std.v index 09cb3ca0c2..695ea26444 100644 --- a/theories/Std.v +++ b/theories/Std.v @@ -134,6 +134,8 @@ Ltac2 @ external cbv : red_flags -> clause -> unit := "ltac2" "tac_cbv". Ltac2 @ external cbn : red_flags -> clause -> unit := "ltac2" "tac_cbn". Ltac2 @ external lazy : red_flags -> clause -> unit := "ltac2" "tac_lazy". +Ltac2 @ external rewrite : evar_flag -> rewriting list -> clause -> (unit -> unit) option -> unit := "ltac2" "tac_rewrite". + Ltac2 @ external reflexivity : unit -> unit := "ltac2" "tac_reflexivity". Ltac2 @ external assumption : unit -> unit := "ltac2" "tac_assumption". |