From a62c7d7ebd7c650710c8a48eec8dab6b7f18f26e Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 4 Jan 2008 15:06:59 +0000 Subject: 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 --- interp/implicit_quantifiers.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'interp') 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 -- cgit v1.2.3