diff options
| author | msozeau | 2008-01-15 01:02:48 +0000 |
|---|---|---|
| committer | msozeau | 2008-01-15 01:02:48 +0000 |
| commit | 6cd832e28c48382cc9321825cc83db36f96ff8d5 (patch) | |
| tree | 51905b3dd36672bf17eeb6e82d45d26402800d7d /interp/implicit_quantifiers.mli | |
| parent | d581efa789d7239b61d7c71f58fc980c350b2de1 (diff) | |
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
Diffstat (limited to 'interp/implicit_quantifiers.mli')
| -rw-r--r-- | interp/implicit_quantifiers.mli | 12 |
1 files changed, 10 insertions, 2 deletions
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 |