Made names of existential variables interpretable as Ltac variables.

This concerns e.g. "?[id]", "?[?id]" or "?id" (in terms, not in
patterns), so that all names occurring in terms are consistently
interpreted as ltac names.

Moreover, with that, we can for instance do:

Ltac pick x := eexists ?[x].
Goal exists x, x = 0.
pick foo.

1 files changed, 12 insertions, 10 deletions

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 =