Fixing #4221 (interpreting bound variables using ltac env was possibly

capturing bound names unexpectingly).

We moved renaming to after finding bindings, i.e. in pretyping
"fun x y => x + y" in an ltac environment where y is ltac-bound to x,
we type the body in environment "x y |-" but build "fun y y => Rel 2 + Rel 1"
(which later on is displayed into "fun y y0 => y + y0").

We renounced to renaming in "match" patterns, which was anyway not
working well, as e.g. in

let x := ipattern:y in (forall z, match z with S x => x | x => x end = 0).

which was producing

forall z : nat, match z with 0 => z | S y => y end = 0

because the names in default branches are treated specifically.

It would be easy to support renaming in match again, by putting the
ltac env in the Cases.pattern_matching_problem state and to rename the
names in "typs" (from build_branch), just before returning them at the
end of the function (and similarly in abstract_predicate for the names
occurring in the return predicate).

However, we rename binders in fix which were not interpreted.

There are some difficulties with evar because we want them defined in
the interpreted env (see comment to ltac_interp_name_env).

fix ltac name

4 files changed, 65 insertions, 32 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 03fe2122c..a212735c0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -270,6 +270,18 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function
                            str"It cannot be used in a binder.")
         else n
 
+let ltac_interp_name_env k0 lvar env =
+  (* envhd is the initial part of the env when pretype was called first *)
+  (* (in practice is is probably 0, but we have to grant the
+     specification of pretype which accepts to start with a non empty
+     rel_context) *)
+  (* tail is the part of the env enriched by pretyping *)
+  let n = rel_context_length (rel_context env) - k0 in
+  let ctxt,_ = List.chop n (rel_context env) in
+  let env = pop_rel_context n env in
+  let ctxt = List.map (fun (na,c,t) -> ltac_interp_name lvar na,c,t) ctxt in
+  push_rel_context ctxt env
+
 let invert_ltac_bound_name lvar env id0 id =
   let id = Id.Map.find id lvar.ltac_idents in
   try mkRel (pi1 (lookup_rel_id id (rel_context env)))
@@ -289,10 +301,6 @@ let pretype_id pretype loc env evdref lvar id =
   let sigma = !evdref in
   (* Look for the binder of [id] *)
   try
-    let id =
-      try Id.Map.find id lvar.ltac_idents
-      with Not_found -> id
-    in
     let (n,_,typ) = lookup_rel_id id (rel_context env) in
       { uj_val  = mkRel n; uj_type = lift n typ }
   with Not_found ->
@@ -413,10 +421,10 @@ let is_GHole = function
 
 let evars = ref Id.Map.empty
 
-let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t =
+let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t =
   let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
-  let pretype_type = pretype_type resolve_tc in
-  let pretype = pretype resolve_tc in
+  let pretype_type = pretype_type k0 resolve_tc in
+  let pretype = pretype k0 resolve_tc in
   match t with
   | GRef (loc,ref,u) ->
       inh_conv_coerce_to_tycon loc env evdref
@@ -436,12 +444,13 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
         with Not_found ->
           user_err_loc (loc,"",str "Unknown existential variable.") in
       let hyps = evar_filtered_context (Evd.find !evdref evk) in
-      let args = pretype_instance resolve_tc env evdref lvar loc hyps evk inst in
+      let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in
       let c = mkEvar (evk, args) in
       let j = (Retyping.get_judgment_of env !evdref c) in
 	inh_conv_coerce_to_tycon loc env evdref j tycon
 
   | GPatVar (loc,(someta,n)) ->
+    let env = ltac_interp_name_env k0 lvar env in
     let ty =
       match tycon with
       | Some ty -> ty
@@ -450,6 +459,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
       { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
 
   | GHole (loc, k, naming, None) ->
+      let env = ltac_interp_name_env k0 lvar env in
       let ty =
         match tycon with
         | Some ty -> ty
@@ -458,6 +468,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
         { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty }
 
   | GHole (loc, k, _naming, Some arg) ->
+      let env = ltac_interp_name_env k0 lvar env in
       let ty =
         match tycon with
         | Some ty -> ty
@@ -474,12 +485,14 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
       | (na,bk,None,ty)::bl ->
         let ty' = pretype_type empty_valcon env evdref lvar ty in
         let dcl = (na,None,ty'.utj_val) in
-	  type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
+        let dcl' = (ltac_interp_name lvar na,None,ty'.utj_val) in
+	  type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl
       | (na,bk,Some bd,ty)::bl ->
         let ty' = pretype_type empty_valcon env evdref lvar ty in
         let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in
         let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
-	  type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
+        let dcl' = (ltac_interp_name lvar na,Some bd'.uj_val,ty'.utj_val) in
+	  type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl in
     let ctxtv = Array.map (type_bl env empty_rel_context) bl in
     let larj =
       Array.map2
@@ -647,9 +660,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     (* The name specified by ltac is used also to create bindings. So
        the substitution must also be applied on variables before they are
        looked up in the rel context. *)
-    let name = ltac_interp_name lvar name in
     let var = (name,None,j.utj_val) in
     let j' = pretype rng (push_rel var env) evdref lvar c2 in
+    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
 
@@ -658,7 +671,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     (* The name specified by ltac is used also to create bindings. So
        the substitution must also be applied on variables before they are
        looked up in the rel context. *)
-    let name = ltac_interp_name lvar name in
     let j' = match name with
       | Anonymous ->
         let j = pretype_type empty_valcon env evdref lvar c2 in
@@ -668,6 +680,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
         let env' = push_rel_assum var env in
           pretype_type empty_valcon env' evdref lvar c2
     in
+    let name = ltac_interp_name lvar name in
     let resj =
       try
         judge_of_product env name j j'
@@ -689,10 +702,10 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     (* The name specified by ltac is used also to create bindings. So
        the substitution must also be applied on variables before they are
        looked up in the rel context. *)
-    let name = ltac_interp_name lvar name in
     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
+    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 }
 
@@ -712,8 +725,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     if not (Int.equal (List.length nal) cs.cs_nargs) then
       user_err_loc (loc,"", str "Destructing let on this type expects " ++ 
 	int cs.cs_nargs ++ str " variables.");
-    let nal = List.map (fun na -> ltac_interp_name lvar na) nal in
-    let na = ltac_interp_name lvar na in
     let fsign, record = 
       match get_projections env indf with
       | None -> List.map2 (fun na (_,c,t) -> (na,c,t))
@@ -729,10 +740,12 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	    (na, c, t) :: aux (n+1) k names l
 	  | [], [] -> []
 	  | _ -> assert false
-	in aux 1 1 (List.rev nal) cs.cs_args, true
-    in
+	in aux 1 1 (List.rev nal) cs.cs_args, true in
     let obj ind p v f =
       if not record then 
+        let nal = List.map (fun na -> ltac_interp_name lvar na) nal in
+        let nal = List.rev nal in
+        let fsign = List.map2 (fun na (_,b,t) -> (na,b,t)) nal fsign in
 	let f = it_mkLambda_or_LetIn f fsign in
 	let ci = make_case_info env (fst ind) LetStyle in
 	  mkCase (ci, p, cj.uj_val,[|f|]) 
@@ -818,7 +831,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	| None ->
 	  let p = match tycon with
 	    | Some ty -> ty
-	    | None -> new_type_evar env evdref loc
+	    | None ->
+              let env = ltac_interp_name_env k0 lvar env in
+              new_type_evar env evdref loc
 	  in
 	    it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
       let pred = nf_evar !evdref pred in
@@ -854,9 +869,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
       inh_conv_coerce_to_tycon loc env evdref cj tycon
 
   | GCases (loc,sty,po,tml,eqns) ->
-    let (tml,eqns) =
-      Glob_ops.map_pattern_binders (fun na -> ltac_interp_name lvar na) tml eqns
-    in
     Cases.compile_cases loc sty
       ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
       tycon env (* loc *) (po,tml,eqns)
@@ -903,13 +915,13 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	  { uj_val = v; uj_type = tval }
     in inh_conv_coerce_to_tycon loc env evdref cj tycon
 
-and pretype_instance resolve_tc env evdref lvar loc hyps evk update =
+and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
   let f (id,_,t) (subst,update) =
     let t = replace_vars subst t in
     let c, update =
       try
         let c = List.assoc id update in
-        let c = pretype resolve_tc (mk_tycon t) env evdref lvar c in
+        let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c in
         c.uj_val, List.remove_assoc id update
       with Not_found ->
       try
@@ -929,7 +941,7 @@ and pretype_instance resolve_tc env evdref lvar loc hyps evk update =
   Array.map_of_list snd subst
 
 (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
-and pretype_type resolve_tc valcon env evdref lvar = function
+and pretype_type k0 resolve_tc valcon env evdref lvar = function
   | GHole (loc, knd, naming, None) ->
       (match valcon with
        | Some v ->
@@ -945,11 +957,12 @@ and pretype_type resolve_tc valcon env evdref lvar = function
 	     { utj_val = v;
 	       utj_type = s }
        | None ->
+           let env = ltac_interp_name_env k0 lvar env in
 	   let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in
 	     { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s);
 	       utj_type = s})
   | c ->
-      let j = pretype resolve_tc empty_tycon env evdref lvar c in
+      let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in
       let loc = loc_of_glob_constr c in
       let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
 	match valcon with
@@ -962,13 +975,14 @@ and pretype_type resolve_tc valcon env evdref lvar = function
 
 let ise_pretype_gen flags env sigma lvar kind c =
   let evdref = ref sigma in
+  let k0 = rel_context_length (rel_context env) in
   let c' = match kind with
     | WithoutTypeConstraint ->
-        (pretype flags.use_typeclasses empty_tycon env evdref lvar c).uj_val
+        (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val
     | OfType exptyp ->
-	(pretype flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val
+	(pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val
     | IsType ->
-	(pretype_type flags.use_typeclasses empty_valcon env evdref lvar c).utj_val 
+	(pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val 
   in
   process_inference_flags flags env sigma (!evdref,c')
 
@@ -1003,14 +1017,16 @@ let on_judgment f j =
 
 let understand_judgment env sigma c =
   let evdref = ref sigma in
-  let j = pretype true empty_tycon env evdref empty_lvar c in
+  let k0 = rel_context_length (rel_context env) in
+  let j = pretype k0 true empty_tycon env evdref empty_lvar c in
   let j = on_judgment (fun c ->
     let evd, c = process_inference_flags all_and_fail_flags env sigma (!evdref,c) in 
       evdref := evd; c) j
   in j, Evd.evar_universe_context !evdref
 
 let understand_judgment_tcc env evdref c =
-  let j = pretype true empty_tycon env evdref empty_lvar c in
+  let k0 = rel_context_length (rel_context env) in
+  let j = pretype k0 true empty_tycon env evdref empty_lvar c in
   on_judgment (fun c ->
     let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in
     evdref := evd; c) j
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 142b54513..a6aa08657 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -123,11 +123,11 @@ val check_evars_are_solved :
 (**/**)
 (** Internal of Pretyping... *)
 val pretype :
-  bool -> type_constraint -> env -> evar_map ref ->
+  int -> bool -> type_constraint -> env -> evar_map ref ->
   ltac_var_map -> glob_constr -> unsafe_judgment
 
 val pretype_type :
-  bool -> val_constraint -> env -> evar_map ref ->
+  int -> bool -> val_constraint -> env -> evar_map ref ->
   ltac_var_map -> glob_constr -> unsafe_type_judgment
 
 val ise_pretype_gen :
diff --git a/test-suite/bugs/closed/4221.v b/test-suite/bugs/closed/4221.v
new file mode 100644
index 000000000..bc120fb1f
--- /dev/null
+++ b/test-suite/bugs/closed/4221.v
@@ -0,0 +1,9 @@
+(* Some test checking that interpreting binder names using ltac
+   context does not accidentally break the bindings *)
+
+Goal (forall x : nat, x = 1 -> False) -> 1 = 1 -> False.
+  intros H0 x.
+  lazymatch goal with
+    | [ x : forall k : nat, _ |- _ ]
+      => specialize (fun H0 => x 1 H0)
+  end.
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index badce063e..952f35bc3 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -298,3 +298,11 @@ evar(foo:nat).
 let evval := eval compute in foo in not_eq evval 1.
 let evval := eval compute in foo in not_eq 1 evval.
 Abort.
+
+(* Check instantiation of binders using ltac names *)
+
+Goal True.
+let x := ipattern:y in assert (forall x y, x = y + 0).
+intro.
+destruct y. (* Check that the name is y here *).
+Abort.