From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- kernel/mod_subst.mli | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'kernel/mod_subst.mli') diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index b14d3920..2e5211c7 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 @@ -147,6 +147,9 @@ val subst_con_kn : val subst_constant : substitution -> Constant.t -> Constant.t +val subst_proj_repr : substitution -> Projection.Repr.t -> Projection.Repr.t +val subst_proj : substitution -> Projection.t -> Projection.t + (** Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? Does the user mean "Unfold X.t" or does she mean "Unfold y" -- cgit v1.2.3