Introducing the remember tactic.

4 files changed, 44 insertions, 0 deletions

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 0db71fb293..e253cc382b 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -303,6 +303,22 @@ let () = define_prim3 "tac_set" begin fun ev p cl ->
   Tactics.letin_pat_tac ev None na (sigma, c) cl
 end
 
+let () = define_prim5 "tac_remember" begin fun ev na c eqpat cl ->
+  let ev = Value.to_bool ev in
+  let na = to_name na in
+  let cl = to_clause cl in
+  let eqpat = Value.to_option to_intro_pattern eqpat in
+  let eqpat = Option.default (IntroNaming IntroAnonymous) eqpat in
+  match eqpat with
+  | IntroNaming eqpat ->
+    Proofview.tclEVARMAP >>= fun sigma ->
+    thaw c >>= fun c ->
+    let c = Value.to_constr c in
+    Tactics.letin_pat_tac ev (Some (true, Loc.tag eqpat)) na (sigma, c) cl
+  | _ ->
+    Tacticals.New.tclZEROMSG (Pp.str "Invalid pattern for remember")
+end
+
 let () = define_prim3 "tac_destruct" begin fun ev ic using ->
   let ev = Value.to_bool ev in
   let ic = Value.to_list to_induction_clause ic in
diff --git a/tests/example2.v b/tests/example2.v
index b667e19bbd..a21f3a7f4e 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -222,3 +222,9 @@ set ($x := True) in * |-.
 constructor.
 Qed.
 
+Goal 0 = 0.
+Proof.
+remember 0 as n eqn: foo at 1.
+rewrite foo.
+reflexivity.
+Qed.
diff --git a/theories/Notations.v b/theories/Notations.v
index 65b05113ae..1b5792e051 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -291,6 +291,26 @@ Ltac2 Notation "set" p(thunk(pose)) cl(opt(clause)) :=
 Ltac2 Notation "eset" p(thunk(pose)) cl(opt(clause)) :=
   Std.set true p (default_on_concl cl).
 
+Ltac2 default_everywhere cl :=
+match cl with
+| None => { Std.on_hyps := None; Std.on_concl := Std.AllOccurrences }
+| Some cl => cl
+end.
+
+Ltac2 Notation "remember"
+  c(thunk(open_constr))
+  na(opt(seq("as", ident)))
+  pat(opt(seq("eqn", ":", intropattern)))
+  cl(opt(clause)) :=
+  Std.remember false na c pat (default_everywhere cl).
+
+Ltac2 Notation "eremember"
+  c(thunk(open_constr))
+  na(opt(seq("as", ident)))
+  pat(opt(seq("eqn", ":", intropattern)))
+  cl(opt(clause)) :=
+  Std.remember true na c pat (default_everywhere cl).
+
 Ltac2 induction0 ev ic use :=
   let f ev use := Std.induction ev ic use in
   enter_h ev f use.
diff --git a/theories/Std.v b/theories/Std.v
index 42bd9edde0..e938bc24b1 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -137,6 +137,8 @@ Ltac2 @ external enough : constr -> (unit -> unit) option option -> intro_patter
 Ltac2 @ external pose : ident option -> constr -> unit := "ltac2" "tac_pose".
 Ltac2 @ external set : evar_flag -> (unit -> ident option * constr) -> clause -> unit := "ltac2" "tac_set".
 
+Ltac2 @ external remember : evar_flag -> ident option -> (unit -> constr) -> intro_pattern option -> clause -> unit := "ltac2" "tac_remember".
+
 Ltac2 @ external destruct : evar_flag -> induction_clause list ->
   constr_with_bindings option -> unit := "ltac2" "tac_induction".