Exporting the rewrite tactic.

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".