From 5e909ab948ea3db4b5d734ec1c68198874c9724c Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 16 Dec 2016 18:35:34 +0100
Subject: pre_ident can be bound to Ltac variables.

The use case is to take a hint database as an argument of Ltac or Tactic Notation.
---
 ltac/tacintern.ml | 1 +
 ltac/tacinterp.ml | 7 ++++---
 ltac/tacsubst.ml  | 1 +
 3 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index 763e0dc22e..4b5d87fc3c 100644
--- a/ltac/tacintern.ml
+++ b/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/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 32bcdfb6a4..fda9142eda 100644
--- a/ltac/tacinterp.ml
+++ b/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/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 55de583613..b09bdda65c 100644
--- a/ltac/tacsubst.ml
+++ b/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);
-- 
cgit v1.2.3