diff options
| author | Pierre-Marie Pédrot | 2020-02-14 23:48:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-14 23:48:57 +0100 |
| commit | 4de476c53d85be4dd266cfe5fd5f2ddec9163a5b (patch) | |
| tree | 1f8cb4ea4350ee9dfef0d65a90aebdd3d939c1d5 /kernel/subtyping.ml | |
| parent | bdc8e29d806ab7e9bbd0491bf237890b7934795a (diff) | |
| parent | 0f58738351db02f30ac43ec52517c54b315d5886 (diff) | |
Merge PR #11557: Use thunks to univ instead of lazy constr for template typing
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 0a654adf7f..11c455de73 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -150,8 +150,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 (* nparams done *) (* params_ctxt done because part of the inductive types *) (* Don't check the sort of the type if polymorphic *) - let ty1 = type_of_inductive env ((mib1, p1), inst) in - let ty2 = type_of_inductive env ((mib2, p2), inst) in + let ty1 = type_of_inductive ((mib1, p1), inst) in + let ty2 = type_of_inductive ((mib2, p2), inst) in let cst = check_inductive_type cst p2.mind_typename ty1 ty2 in cst in |