From 6cd832e28c48382cc9321825cc83db36f96ff8d5 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 15 Jan 2008 01:02:48 +0000
Subject: Generalize instance declarations to any context, better name
 handling. Add hole kind info for topconstrs. Derive eta_expansion from
 functional extensionality axiom.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10439 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/implicit_quantifiers.mli | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'interp/implicit_quantifiers.mli')

diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 3e26b6c72a..ab23e763c1 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -23,6 +23,7 @@ open Util
 open Typeclasses
 (*i*)
 
+val ids_of_list : identifier list -> Idset.t
 val destClassApp : constr_expr -> identifier located * constr_expr list
 val destClassAppExpl : constr_expr -> identifier located * (constr_expr * explicitation located option) list
 
@@ -30,6 +31,13 @@ val free_vars_of_constr_expr :     Topconstr.constr_expr ->
     ?bound:Idset.t ->
   Names.identifier list -> Names.identifier list
 
+val binder_list_of_ids : identifier list -> local_binder list
+
+val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
+
+val free_vars_of_binders :
+  ?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list
+
 val compute_constrs_freevars : Idset.t -> constr_expr list -> identifier list
 val compute_constrs_freevars_binders : Idset.t -> constr_expr list -> (identifier located * constr_expr) list
 val resolve_class_binders : Idset.t -> typeclass_context -> 
@@ -51,10 +59,10 @@ val nf_rel_context : evar_map -> rel_context -> rel_context
 val nf_env : evar_map -> env -> env
 
 val combine_params : Names.Idset.t ->
-  (Names.Idset.t -> Names.identifier option * (Names.identifier * Term.constr option * Term.types) ->
+  (Names.Idset.t -> (Names.identifier * bool) option * (Names.identifier * Term.constr option * Term.types) ->
     Topconstr.constr_expr * Names.Idset.t) ->
   (Topconstr.constr_expr * Topconstr.explicitation located option) list ->
-  (Names.identifier option * Term.named_declaration) list ->
+  ((Names.identifier * bool) option * Term.named_declaration) list ->
   Topconstr.constr_expr list * Names.Idset.t
 
 
-- 
cgit v1.2.3