diff options
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 |