Fix name capture bug and call the right pretyper in subtac.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10414 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 20 insertions, 5 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index da91b04062..e6ea17b472 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -62,6 +62,13 @@ let interp_constrs_evars isevars env avoid l =
 	(push_named d env, id :: ids, d::params))
     (env, avoid, []) l
     
+let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
+  SPretyping.understand_tcc_evars evdref env kind
+    (intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c)
+
+let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
+  interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
+
 let type_ctx_instance isevars env ctx inst subst =
   List.fold_left2
     (fun (subst, instctx) (na, _, t) ce ->
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index d9113644cb..7be0b015e8 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -81,9 +81,14 @@ let compute_constrs_freevars_binders env constrs =
   let elts = compute_constrs_freevars env constrs in
     List.map (fun id -> (dummy_loc, id), CHole dummy_loc) elts
       
+let next_ident_away_from id avoid = 
+  let rec name_rec id =
+    if Idset.mem id avoid then name_rec (Nameops.lift_ident id) else id in 
+  name_rec id 
+
 let ids_of_named_context_avoiding avoid l =
   List.fold_left (fun (ids, avoid) id -> 
-    let id' = Nameops.next_ident_away_from id avoid in id' :: ids, id' :: avoid) 
+    let id' = next_ident_away_from id avoid in id' :: ids, Idset.add id' avoid) 
     ([], avoid) (Termops.ids_of_named_context l)
     
 let combine_params avoid applied needed =
@@ -97,8 +102,8 @@ let combine_params avoid applied needed =
   in aux [] applied needed
 
 let compute_context_vars env l =
-  List.fold_left (fun l (iid, _, c) -> 
-    (match snd iid with Name i -> [i] | Anonymous -> []) @ free_vars_of_constr_expr c ~bound:env l)
+  List.fold_left (fun avoid (iid, _, c) -> 
+    (match snd iid with Name i -> [i] | Anonymous -> []) @ (free_vars_of_constr_expr c ~bound:env avoid))
     [] l
 
 let destClassApp cl =
@@ -106,8 +111,11 @@ let destClassApp cl =
     | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l
     | _ -> raise Not_found
 
+let ids_of_list l = 
+  List.fold_right Idset.add l Idset.empty
+
 let full_class_binders env l = 
-  let avoid = compute_context_vars env l in
+  let avoid = Idset.union env (ids_of_list (compute_context_vars env l)) in
   let l', avoid =
     List.fold_left (fun (l', avoid) (iid, bk, cl as x) -> 
       match bk with
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index a61dbcadf5..3b9d98652b 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -27,7 +27,7 @@ val destClassApp : constr_expr -> identifier located * constr_expr list
 
 val free_vars_of_constr_expr :     Topconstr.constr_expr ->
     ?bound:Idset.t ->
-    Names.identifier list -> Names.identifier list
+  Names.identifier list -> Names.identifier list
 
 val compute_constrs_freevars : Idset.t -> constr_expr list -> identifier list
 val compute_constrs_freevars_binders : Idset.t -> constr_expr list -> (identifier located * constr_expr) list