diff options
Diffstat (limited to 'kernel/mod_subst.mli')
| -rw-r--r-- | kernel/mod_subst.mli | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 7164d1162..91139985b 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -19,10 +19,11 @@ type substitution val empty_delta_resolver : delta_resolver -val add_inline_delta_resolver : constant -> delta_resolver -> delta_resolver +val add_inline_delta_resolver : + constant -> int -> delta_resolver -> delta_resolver -val add_inline_constr_delta_resolver : constant -> constr -> delta_resolver - -> delta_resolver +val add_inline_constr_delta_resolver : + constant -> int -> constr -> delta_resolver -> delta_resolver val add_constant_delta_resolver : constant -> delta_resolver -> delta_resolver @@ -50,7 +51,7 @@ val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive val delta_of_mp : delta_resolver -> module_path -> module_path (** Extract the set of inlined constant in the resolver *) -val inline_of_delta : delta_resolver -> kernel_name list +val inline_of_delta : int option -> delta_resolver -> (int * kernel_name) list (** remove_mp is used for the computation of a resolver induced by Include P *) val remove_mp_delta_resolver : delta_resolver -> module_path -> delta_resolver |