Merge PR#395: Allow hintdb to be parameters in a Ltac definition or

Tactic Notation

7 files changed, 50 insertions, 12 deletions

diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index a37cf306e1..4ec42c676f 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -149,15 +149,6 @@ TACTIC EXTEND autounfold_one
     [ Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None ]
       END
 
-TACTIC EXTEND autounfoldify
-| [ "autounfoldify" constr(x) ] -> [
-    let db = match Term.kind_of_term x with
-      | Term.Const (c,_) -> Names.Label.to_string (Names.con_label c)
-      | _ -> assert false
-    in Eauto.autounfold ["core";db] Locusops.onConcl 
-  ]
-END
-
 TACTIC EXTEND unify
 | ["unify" constr(x) constr(y) ] -> [ Tactics.unify x y ]
 | ["unify" constr(x) constr(y) "with" preident(base)  ] -> [
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 763e0dc22e..4b5d87fc3c 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -782,6 +782,7 @@ let intern_ltac ist tac =
 let () =
   Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var);
   Genintern.register_intern0 wit_ref (lift intern_global_reference);
+  Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c));
   Genintern.register_intern0 wit_ident intern_ident';
   Genintern.register_intern0 wit_var (lift intern_hyp);
   Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 32bcdfb6a4..fda9142eda 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2023,9 +2023,6 @@ let () =
 let () =
   declare_uniform wit_string
 
-let () =
-  declare_uniform wit_pre_ident
-
 let lift f = (); fun ist x -> Ftactic.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
@@ -2053,9 +2050,13 @@ let interp_destruction_arg' ist c = Ftactic.nf_enter { enter = begin fun gl ->
   Ftactic.return (interp_destruction_arg ist gl c)
 end }
 
+let interp_pre_ident ist env sigma s =
+  s |> Id.of_string |> interp_ident ist env sigma |> Id.to_string
+
 let () =
   register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
   register_interp0 wit_ref (lift interp_reference);
+  register_interp0 wit_pre_ident (lift interp_pre_ident);
   register_interp0 wit_ident (lift interp_ident);
   register_interp0 wit_var (lift interp_hyp);
   register_interp0 wit_intro_pattern (lifts interp_intro_pattern);
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 55de583613..b09bdda65c 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -291,6 +291,7 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) =
 let () =
   Genintern.register_subst0 wit_int_or_var (fun _ v -> v);
   Genintern.register_subst0 wit_ref subst_global_reference;
+  Genintern.register_subst0 wit_pre_ident (fun _ v -> v);
   Genintern.register_subst0 wit_ident (fun _ v -> v);
   Genintern.register_subst0 wit_var (fun _ v -> v);
   Genintern.register_subst0 wit_intro_pattern (fun _ v -> v);
diff --git a/test-suite/bugs/closed/2417.v b/test-suite/bugs/closed/2417.v
new file mode 100644
index 0000000000..b2f00ffc65
--- /dev/null
+++ b/test-suite/bugs/closed/2417.v
@@ -0,0 +1,15 @@
+Parameter x y : nat.
+Axiom H : x = y.
+Hint Rewrite H : mybase.
+
+Ltac bar base := autorewrite with base.
+
+Tactic Notation "foo" ident(base) := autorewrite with base.
+
+Goal x = 0.
+  bar mybase.
+  now_show (y = 0).
+  Undo 2.
+  foo mybase.
+  now_show (y = 0).
+Abort.
diff --git a/test-suite/success/hintdb_in_ltac.v b/test-suite/success/hintdb_in_ltac.v
new file mode 100644
index 0000000000..f12b4d1f45
--- /dev/null
+++ b/test-suite/success/hintdb_in_ltac.v
@@ -0,0 +1,14 @@
+Definition x := 0.
+
+Hint Unfold x : mybase.
+
+Ltac autounfoldify base := autounfold with base.
+
+Tactic Notation "autounfoldify_bis" ident(base) := autounfold with base.
+
+Goal x = 0.
+  progress autounfoldify mybase.
+  Undo.
+  progress autounfoldify_bis mybase.
+  trivial.
+Qed.
diff --git a/test-suite/success/hintdb_in_ltac_bis.v b/test-suite/success/hintdb_in_ltac_bis.v
new file mode 100644
index 0000000000..f5c25540ef
--- /dev/null
+++ b/test-suite/success/hintdb_in_ltac_bis.v
@@ -0,0 +1,15 @@
+Parameter Foo : Prop.
+Axiom H : Foo.
+
+Hint Resolve H : mybase.
+
+Ltac foo base := eauto with base.
+
+Tactic Notation "bar" ident(base) :=
+  typeclasses eauto with base.
+
+Goal Foo.
+  progress foo mybase.
+  Undo.
+  progress bar mybase.
+Qed.
\ No newline at end of file