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 /pretyping/inductiveops.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 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 816a8c4703..a4406aeba1 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -29,7 +29,7 @@ open Context.Rel.Declaration let type_of_inductive env (ind,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in Typeops.check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; - Inductive.type_of_inductive env (specif,u) + Inductive.type_of_inductive (specif,u) (* Return type as quoted by the user *) let type_of_constructor env (cstr,u) = |