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

Tactic Notation

4 files changed, 6 insertions, 12 deletions

diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index a37cf306e..4ec42c676 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 763e0dc22..4b5d87fc3 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 32bcdfb6a..fda9142ed 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 55de58361..b09bdda65 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);