From 7baac26fccbd903f82f09e542aee1aa994d50c0d Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 8 Nov 2009 02:19:44 +0000
Subject: 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
---
 interp/implicit_quantifiers.mli | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'interp/implicit_quantifiers.mli')

diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 8f02eb7658..1feae81f56 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
 
-- 
cgit v1.2.3