aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/mod_subst.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/mod_subst.mli')
-rw-r--r--kernel/mod_subst.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index b14d39207..76a1d173b 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -28,7 +28,7 @@ val add_kn_delta_resolver :
KerName.t -> KerName.t -> delta_resolver -> delta_resolver
val add_inline_delta_resolver :
- KerName.t -> (int * constr option) -> delta_resolver -> delta_resolver
+ KerName.t -> (int * (Univ.AUContext.t * constr) option) -> delta_resolver -> delta_resolver
val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver