diff options
| author | Gaëtan Gilbert | 2018-11-12 12:55:46 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-05 13:20:58 +0100 |
| commit | 470943bdf917caf352b5347c8d33fc39699805b0 (patch) | |
| tree | 02407cc74a5ffe2aa184ebcddb4ea6ab2ea1f920 /kernel/mod_subst.mli | |
| parent | 23f2222bb2c97110b6e55835fd19528177e41ff3 (diff) | |
Fix mod_subst wrt universe polymorphism
Diffstat (limited to 'kernel/mod_subst.mli')
| -rw-r--r-- | kernel/mod_subst.mli | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 8416094063..ea391b3de7 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,17 +133,11 @@ 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 |