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

3 files changed, 18 insertions, 11 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0f593e67c..0057edad6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -842,7 +842,7 @@ let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar
 	Implicit_quantifiers.combine_params_freevar ty
   in
   let ty' = intern_type (ids,true,tmpsc,sc) ty in
-  let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids ty' in
+  let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids ~allowed:ids' ty' in
   let env' = List.fold_left (fun env (x, l) -> push_loc_name_env ~fail_anonymous lvar env l (Name x)) env fvs in
   let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in
   let na = match na with
@@ -879,7 +879,7 @@ let intern_local_binder_aux ?(fail_anonymous=false) intern intern_type lvar ((id
 
 let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c =
   let c = intern (ids,true,tmp_scope,scopes) c in
-  let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids c in
+  let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids c in
   let env', c' =
     let abs =
       let pi =
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index dc2f8ad0a..f9ac88e6b 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 =
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 8f02eb765..1feae81f5 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -38,9 +38,11 @@ val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t ->
 val free_vars_of_binders :
   ?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list
 
-(* Returns the free ids in left-to-right order with the location of their first occurence *)
+(* Returns the generalizable free ids in left-to-right
+   order with the location of their first occurence *)
 
-val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier * loc) list
+val generalizable_vars_of_rawconstr : ?bound:Idset.t -> ?allowed:Idset.t ->
+  rawconstr -> (Names.identifier * loc) list
 
 val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier