diff options
Diffstat (limited to 'kernel/mod_subst.mli')
| -rw-r--r-- | kernel/mod_subst.mli | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 8416094063..8ab3d04402 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 * (Univ.AUContext.t * constr) option) -> delta_resolver -> delta_resolver + KerName.t -> (int * constr Univ.univ_abstracted option) -> delta_resolver -> delta_resolver val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver @@ -133,23 +133,19 @@ val subst_kn : substitution -> KerName.t -> KerName.t val subst_con : - substitution -> pconstant -> Constant.t * constr + substitution -> Constant.t -> Constant.t * constr Univ.univ_abstracted option val subst_pcon : substitution -> pconstant -> pconstant -val subst_pcon_term : - substitution -> pconstant -> pconstant * constr - -val subst_con_kn : - substitution -> Constant.t -> Constant.t * constr - 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 +val subst_retro_action : substitution -> Retroknowledge.action -> Retroknowledge.action + (** 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" |