diff options
| author | Amin Timany | 2017-05-24 13:56:51 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-06-16 04:51:18 +0200 |
| commit | 960b6d7e17d7a44ad2e058a5b24a2628293408bc (patch) | |
| tree | fd38b0523c7b7dfd014b5726ecf8ab3ad9c5810c | |
| parent | c01d225f9e112bb08f9df26f70805bde0c0d127a (diff) | |
Properly instantiate contexts before pushing
| -rw-r--r-- | checker/indtypes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml index cac7e63134..2716489a4f 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -555,8 +555,8 @@ let check_subtyping mib paramsctxt env_ar inds = let dosubst = subst_univs_level_constr sbsubst in let uctx = Univ.UInfoInd.univ_context mib.mind_universes in let uctx_other = Univ.UContext.make (other_instnace, Univ.UContext.constraints uctx) in - let env = Environ.push_context uctx env_ar in - let env = Environ.push_context uctx_other env in + let env = Environ.push_context (Univ.instantiate_univ_context uctx) env_ar in + let env = Environ.push_context (Univ.instantiate_univ_context uctx_other) env in let env = Environ.push_context (Univ.instantiate_univ_context (Univ.UInfoInd.subtyp_context mib.mind_universes)) env in (* process individual inductive types: *) Array.iter (fun { mind_user_lc = lc; mind_arity = arity } -> |