Add partial setoids in theories/Classes, add SetoidDec class for setoids with a decidable equality. Fix name capture bug, again.

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

1 files changed, 8 insertions, 4 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 2de7945ee..c029550a1 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -59,6 +59,9 @@ let is_freevar ids env x =
       with _ -> not (is_global x)
   with _ -> true
 
+let rec make_fresh ids env x =
+  if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_ident x)
+
 let freevars_of_ids env ids = 
   List.filter (is_freevar env (Global.env())) ids
 
@@ -81,10 +84,10 @@ 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 next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id
+(*   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 -> 
@@ -172,6 +175,7 @@ let generalize_class_binders env l =
     cstrs
 
 let generalize_class_binders_raw env l = 
+  let env = Idset.union env (Termops.vars_of_env (Global.env())) in
   let fv_ctx, cstrs = resolve_class_binders env l in
     List.map (fun ((loc, id), t) -> ((loc, Name id), Implicit, t)) fv_ctx,
   List.map (fun (iid, bk, c) -> (iid, Implicit, c)) cstrs