diff options
| author | Maxime Dénès | 2018-06-17 08:19:49 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-17 08:19:49 +0200 |
| commit | 0651bbfa273b2adc027ddd2cfb59df2fc5ea1330 (patch) | |
| tree | 0e909cb9e6bac4e6b46127f88d2ae7d1611ed562 /checker/declarations.ml | |
| parent | cee11fc609cb7d7087adabba389a97991e636219 (diff) | |
| parent | 45e1e0dcba3101b6a9e096f18c28da899615af7f (diff) | |
Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.
Diffstat (limited to 'checker/declarations.ml')
| -rw-r--r-- | checker/declarations.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index e1d2cf6d1d..a744a02279 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -196,7 +196,12 @@ let subst_con0 sub con u = let dup con = con, Const (con, u) in let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in match constant_of_delta_with_inline resolve con' with - | Some t -> con', t + | Some (ctx, t) -> + (** FIXME: we never typecheck the inlined term, so that it could well + be garbage. What environment do we type it in though? The substitution + code should be moot in the checker but it **is** used nonetheless. *) + let () = assert (Univ.AUContext.size ctx == Univ.Instance.length u) in + con', subst_instance_constr u t | None -> let con'' = match side with | User -> constant_of_delta resolve con' @@ -340,7 +345,7 @@ let gen_subst_delta_resolver dom subst resolver = let kkey' = if dom then subst_kn subst kkey else kkey in let hint' = match hint with | Equiv kequ -> Equiv (subst_kn_delta subst kequ) - | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t)) + | Inline (lev,Some (ctx, t)) -> Inline (lev,Some (ctx, subst_mps subst t)) | Inline (_,None) -> hint in Deltamap.add_kn kkey' hint' rslv |