Ltac's [uconstr] values now use the identifier context to give names to binders.

It does not work fine for refine yet as, while the binder has indeed the correct name, the evars are pretyped in an environment with the Ltac name, hence goal do not display the appropriate name.

3 files changed, 11 insertions, 5 deletions

diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index ec27aab338..b4543bb59b 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -77,6 +77,7 @@ and cases_clauses = cases_clause list
     of its free variables. Intended for use when these variables are taken
     from the Ltac environment. *)
 type closure = {
+  idents:Id.t Id.Map.t;
   typed: Pattern.constr_under_binders Id.Map.t ;
   untyped:closed_glob_constr Id.Map.t }
 and closed_glob_constr = {
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ff0d89a5c3..698f465593 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -370,6 +370,7 @@ let refine_tac {Glob_term.closure=closure;term=term} =
     let lvar = { Pretyping.empty_lvar with
       Pretyping.ltac_constrs = closure.Glob_term.typed;
       Pretyping.ltac_uconstrs = closure.Glob_term.untyped;
+      Pretyping.ltac_idents = closure.Glob_term.idents;
     } in
     let update evd = Pretyping.understand_ltac flags evd env lvar tycon term in
     Proofview.Refine.refine_casted (fun h -> Proofview.Refine.update h update) <*>
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 7d606402b0..00ca189591 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -462,17 +462,21 @@ let interp_fresh_id ist env l =
 (* Extract the uconstr list from lfun *)
 let extract_ltac_uconstr_values ist env =
   let open Glob_term in
-  let fold id v ({typed;untyped} as accu) =
+  let fold id v ({idents;typed;untyped} as accu) =
     try
       let c = coerce_to_uconstr env v in
-      { typed ; untyped = Id.Map.add id c untyped }
+      { idents ; typed ; untyped = Id.Map.add id c untyped }
     with CannotCoerceTo _ -> try
       let c = coerce_to_constr env v in
-      { typed = Id.Map.add id c typed ; untyped }
+      { idents ; typed = Id.Map.add id c typed ; untyped }
+    with CannotCoerceTo _ -> try
+      let id' = coerce_to_ident false env v in
+      { idents = Id.Map.add id id' idents ; typed ; untyped }
     with CannotCoerceTo _ ->
       accu
   in
-  Id.Map.fold fold ist.lfun { typed = Id.Map.empty ; untyped = Id.Map.empty }
+  let empty =  { idents = Id.Map.empty ;typed = Id.Map.empty ; untyped = Id.Map.empty } in
+  Id.Map.fold fold ist.lfun empty
 
 (** Significantly simpler than [interp_constr], to interpret an
     untyped constr, it suffices to adjoin a closure environment. *)
@@ -1314,7 +1318,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_idents = closure.idents;
           Pretyping.ltac_genargs = ist.lfun;
         } in
         let (sigma,c_interp) =