Merge PR #7309: Made names of existential variables interpretable as Ltac variables.

5 files changed, 54 insertions, 10 deletions

diff --git a/CHANGES b/CHANGES
index 29b8fa1094..9f3bdcedae 100644
--- a/CHANGES
+++ b/CHANGES
@@ -73,6 +73,10 @@ Tactics
 
 - The `romega` tactics have been deprecated; please use `lia` instead.
 
+- Names of existential variables occurring in Ltac functions
+  (e.g. "?[n]" or "?n" in terms - not in patterns) are now interpreted
+  the same way as other variable names occurring in Ltac functions.
+
 Focusing
 
 - Focusing bracket `{` now supports named goal selectors,
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 12788e5ec5..25510826cc 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -55,16 +55,16 @@ let env env = env.static_env
 let vars_of_env env =
   Id.Set.union (Id.Map.domain env.lvar.ltac_genargs) (vars_of_env env.static_env)
 
-let ltac_interp_name { ltac_idents ; ltac_genargs } = function
-  | Anonymous -> Anonymous
-  | Name id as na ->
-      try Name (Id.Map.find id ltac_idents)
-      with Not_found ->
-        if Id.Map.mem id ltac_genargs then
-          user_err (str "Ltac variable" ++ spc () ++ Id.print id ++
-                    spc () ++ str "is not bound to an identifier." ++
-                    spc () ++str "It cannot be used in a binder.")
-        else na
+let ltac_interp_id { ltac_idents ; ltac_genargs } id =
+  try Id.Map.find id ltac_idents
+  with Not_found ->
+    if Id.Map.mem id ltac_genargs then
+      user_err (str "Ltac variable" ++ spc () ++ Id.print id ++
+                spc () ++ str "is not bound to an identifier." ++
+                spc () ++str "It cannot be used in a binder.")
+    else id
+
+let ltac_interp_name lvar = Nameops.Name.map (ltac_interp_id lvar)
 
 let push_rel sigma d env =
   let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in
@@ -182,6 +182,8 @@ let interp_ltac_variable ?loc typing_fun env sigma id =
   end;
   raise Not_found
 
+let interp_ltac_id env id = ltac_interp_id env.lvar id
+
 module ConstrInterpObj =
 struct
   type ('r, 'g, 't) obj =
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli
index 4038523211..70a7ee6e2f 100644
--- a/pretyping/globEnv.mli
+++ b/pretyping/globEnv.mli
@@ -76,6 +76,11 @@ val hide_variable : t -> Name.t -> Id.t -> t
 val interp_ltac_variable : ?loc:Loc.t -> (t -> Glob_term.glob_constr -> unsafe_judgment) ->
   t -> evar_map -> Id.t -> unsafe_judgment
 
+(** Interp an identifier as an ltac variable bound to an identifier,
+    or as the identifier itself if not bound to an ltac variable *)
+
+val interp_ltac_id : t -> Id.t -> Id.t
+
 (** Interpreting a generic argument, typically a "ltac:(...)", taking
     into account the possible renaming *)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e3aa90fbcf..a4c2cb2352 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -480,6 +480,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
   | GEvar (id, inst) ->
       (* Ne faudrait-il pas s'assurer que hyps est bien un
 	 sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
+      let id = interp_ltac_id env id in
       let evk =
         try Evd.evar_key id !evdref
         with Not_found ->
@@ -499,6 +500,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
       { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
 
   | GHole (k, naming, None) ->
+      let open Namegen in
+      let naming = match naming with
+        | IntroIdentifier id -> IntroIdentifier (interp_ltac_id env id)
+        | IntroAnonymous -> IntroAnonymous
+        | IntroFresh id -> IntroFresh (interp_ltac_id env id) in
       let ty =
         match tycon with
         | Some ty -> ty
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 4404ff3f16..448febed25 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -377,3 +377,30 @@ f y true.
 Abort.
 
 End LtacNames.
+
+(* Test binding of the name of existential variables in Ltac *)
+
+Module EvarNames.
+
+Ltac pick x := eexists ?[x].
+Goal exists y, y = 0.
+pick foo.
+[foo]:exact 0.
+auto.
+Qed.
+
+Ltac goal x := refine ?[x].
+
+Goal forall n, n + 0 = n.
+Proof.
+  induction n; [ goal Base | goal Rec ].
+  [Base]: {
+    easy.
+  }
+  [Rec]: {
+    simpl.
+    now f_equal.
+  }
+Qed.
+
+End EvarNames.