diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
| commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
| tree | 0c647056de1832cf1dba5ba58758b9121418e4be /interp/implicit_quantifiers.mli | |
| parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) | |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'interp/implicit_quantifiers.mli')
| -rw-r--r-- | interp/implicit_quantifiers.mli | 19 |
1 files changed, 6 insertions, 13 deletions
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index ff81dc10..1ee81ce9 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: implicit_quantifiers.mli 10739 2008-04-01 14:45:20Z herbelin $ i*) +(*i $Id: implicit_quantifiers.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Names @@ -39,30 +39,23 @@ 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 -> (identifier located * constr_expr) list * typeclass_context val full_class_binders : Idset.t -> typeclass_context -> typeclass_context + +val generalize_class_binder_raw : Idset.t -> name located * (binding_kind * binding_kind) * constr_expr -> + Idset.t * typeclass_context * typeclass_constraint val generalize_class_binders_raw : Idset.t -> typeclass_context -> (name located * binding_kind * constr_expr) list * (name located * binding_kind * constr_expr) list -val ctx_of_class_binders : Idset.t -> typeclass_context -> local_binder list - -val implicits_of_binders : local_binder list -> (Topconstr.explicitation * (bool * bool)) list - val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list val combine_params : Names.Idset.t -> - (Names.Idset.t -> (global_reference * bool) option * (Names.identifier * Term.constr option * Term.types) -> + (Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) -> Topconstr.constr_expr * Names.Idset.t) -> (Topconstr.constr_expr * Topconstr.explicitation located option) list -> - ((global_reference * bool) option * Term.named_declaration) list -> + ((global_reference * bool) option * Term.rel_declaration) list -> Topconstr.constr_expr list * Names.Idset.t - -val ids_of_named_context_avoiding : Names.Idset.t -> - Sign.named_context -> Names.Idset.elt list * Names.Idset.t - |