diff options
| author | msozeau | 2009-11-08 02:19:44 +0000 |
|---|---|---|
| committer | msozeau | 2009-11-08 02:19:44 +0000 |
| commit | 7baac26fccbd903f82f09e542aee1aa994d50c0d (patch) | |
| tree | 38c64e213733727fb82f0c1ae8e6362226a9fcce /interp/implicit_quantifiers.ml | |
| parent | 6d684ec32bc62ff1e9528081a2369852cc5b5c65 (diff) | |
Use generalizable variables info when internalizing arbitrary bindings,
not just type class applications.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12479 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index dc2f8ad0aa..f9ac88e6bc 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -95,13 +95,17 @@ let is_freevar ids env x = (* Auxilliary functions for the inference of implicitly quantified variables. *) +let ungeneralizable loc id = + user_err_loc (loc, "Generalization", + str "Unbound and ungeneralizable variable " ++ pr_id id) + let free_vars_of_constr_expr c ?(bound=Idset.empty) l = let found loc id bdvars l = if List.mem id l then l else if is_freevar bdvars (Global.env ()) id then if find_generalizable_ident id then id :: l - else user_err_loc (loc, "Generalization", str "Unbound and ungeneralizable variable " ++ pr_id id) + else ungeneralizable loc id else l in let rec aux bdvars l c = match c with @@ -134,7 +138,7 @@ let add_name_to_ids set na = | Anonymous -> set | Name id -> Idset.add id set -let free_vars_of_rawconstr ?(bound=Idset.empty) = +let generalizable_vars_of_rawconstr ?(bound=Idset.empty) ?(allowed=Idset.empty) = let rec vars bound vs = function | RVar (loc,id) -> if is_freevar bound (Global.env ()) id then @@ -191,15 +195,16 @@ let free_vars_of_rawconstr ?(bound=Idset.empty) = and vars_return_type bound vs (na,tyopt) = let bound' = add_name_to_ids bound na in vars_option bound' vs tyopt - in - fun rt -> List.rev (vars bound [] rt) + in fun rt -> + let vars = List.rev (vars bound [] rt) in + List.iter (fun (id, loc) -> + if not (Idset.mem id allowed || find_generalizable_ident id) then + ungeneralizable loc id) vars; + vars 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 fre_ids env ids = - List.filter (is_freevar env (Global.env())) ids - let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id let next_name_away_from na avoid = |