Adds an identifier context in pretying's Ltac context.

Binder names are interpreted as the Ltac specified one if available.

4 files changed, 29 insertions, 1 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 56a6671152..641d3669a7 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -51,6 +51,7 @@ type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t
 type ltac_var_map = {
   ltac_constrs : var_map;
   ltac_uconstrs : uconstr_var_map;
+  ltac_idents: Id.t Id.Map.t;
   ltac_genargs : unbound_ltac_var_map;
 }
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
@@ -227,6 +228,17 @@ let orelse_name name name' = match name with
   | Anonymous -> name'
   | _ -> name
 
+let ltac_interp_name { ltac_idents ; ltac_genargs } = function
+  | Anonymous -> Anonymous
+  | Name id as n ->
+      try Name (Id.Map.find id ltac_idents)
+      with Not_found ->
+        if Id.Map.mem id ltac_genargs then
+          errorlabstrm "" (str"Ltac variable"++spc()++ pr_id id ++
+                           spc()++str"is not bound to an identifier."++spc()++
+                           str"It cannot be used in a binder.")
+        else n
+
 let invert_ltac_bound_name env id0 id =
   try mkRel (pi1 (lookup_rel_id id (rel_context env)))
   with Not_found ->
@@ -635,6 +647,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     let j = pretype_type dom_valcon env evdref lvar c1 in
     let var = (name,None,j.utj_val) in
     let j' = pretype rng (push_rel var env) evdref lvar c2 in
+    (* The name specified by ltac is used only *after* pretying, when all bound
+       names have been resolved to rels. *)
+    let name = ltac_interp_name lvar name in
     let resj = judge_of_abstraction env (orelse_name name name') j j' in
       inh_conv_coerce_to_tycon loc env evdref resj tycon
 
@@ -650,7 +665,11 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
           pretype_type empty_valcon env' evdref lvar c2
     in
     let resj =
-      try judge_of_product env name j j'
+      try
+        (* The name specified by ltac is used only *after* pretying, when all bound
+           names have been resolved to rels. *)
+        let name = ltac_interp_name lvar name in
+        judge_of_product env name j j'
       with TypeError _ as e -> let e = Errors.push e in Loc.raise loc e in
       inh_conv_coerce_to_tycon loc env evdref resj tycon
 
@@ -666,6 +685,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     let var = (name,Some j.uj_val,t) in
     let tycon = lift_tycon 1 tycon in
     let j' = pretype tycon (push_rel var env) evdref lvar c2 in
+    (* The name specified by ltac is used only *after* pretying, when all bound
+       names have been resolved to rels. *)
+    let name = ltac_interp_name lvar name in
       { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
 	uj_type = subst1 j.uj_val j'.uj_type }
 
@@ -933,6 +955,7 @@ let all_no_fail_flags = default_inference_flags false
 let empty_lvar : ltac_var_map = {
   ltac_constrs = Id.Map.empty;
   ltac_uconstrs = Id.Map.empty;
+  ltac_idents = Id.Map.empty;
   ltac_genargs = Id.Map.empty;
 }
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 33f5e420d2..695b2b51f0 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -36,6 +36,8 @@ type ltac_var_map = {
   (** Ltac variables bound to constrs *)
   ltac_uconstrs : uconstr_var_map;
   (** Ltac variables bound to untyped constrs *)
+  ltac_idents: Id.t Id.Map.t;
+  (** Ltac variables bound to identifiers *)
   ltac_genargs : unbound_ltac_var_map;
   (** Ltac variables bound to other kinds of arguments *)
 }
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 478019b41e..ace595a7bd 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -47,6 +47,7 @@ let instantiate_tac n (ist,rawc) ido =
     let lvar = {
       Pretyping.ltac_constrs = constrvars;
       ltac_uconstrs = Names.Id.Map.empty;
+      ltac_idents = Names.Id.Map.empty;
       ltac_genargs = ist.Geninterp.lfun;
     } in
     let sigma' = w_refine (evk,evi) (lvar ,rawc) sigma in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5b0002d7e5..7d606402b0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -492,6 +492,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   let vars = {
     Pretyping.ltac_constrs = constrvars;
     Pretyping.ltac_uconstrs = Id.Map.empty;
+    Pretyping.ltac_idents = Id.Map.empty;
     Pretyping.ltac_genargs = ist.lfun;
   } in
   let c = match ce with
@@ -1313,6 +1314,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
         let vars = {
           Pretyping.ltac_constrs = closure.typed;
           Pretyping.ltac_uconstrs = closure.untyped;
+          Pretyping.ltac_idents = Id.Map.empty;
           Pretyping.ltac_genargs = ist.lfun;
         } in
         let (sigma,c_interp) =