diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-05-03 11:21:47 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:17 +0200 |
| commit | 763f5d5d5c6f8b798cc138d0c68fffcb7c544e41 (patch) | |
| tree | 6a76d241b23be331b14016a103fe3580b6a4daa6 /checker/indtypes.ml | |
| parent | d6898781f9cd52ac36a4891d7b169ddab7b8af50 (diff) | |
Correct coqchk checking subtyping relation for inductives
Diffstat (limited to 'checker/indtypes.ml')
| -rw-r--r-- | checker/indtypes.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 00ff447cc..69dd6f57a 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -551,10 +551,10 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : con let check_subtyping mib paramsctxt env_ar inds = let numparams = rel_context_nhyps paramsctxt in let sbsubst = Univ.UInfoInd.subtyping_susbst mib.mind_universes in - let dosubst = subst_univs_level_constr sbsubst in + let dosubst = subst_instance_constr sbsubst in let uctx = Univ.UInfoInd.univ_context mib.mind_universes in - let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in - let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in + let instance_other = Univ.subst_instance_instance sbsubst (Univ.UContext.instance uctx) in + let constraints_other = Univ.subst_instance_constraints sbsubst (Univ.UContext.constraints uctx) in let uctx_other = Univ.UContext.make (instance_other, constraints_other) in let env' = Environ.push_context uctx env_ar in let env'' = Environ.push_context uctx_other env' in |