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 /vernac/record.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 'vernac/record.ml')
| -rw-r--r-- | vernac/record.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index 27bd390714..3e44cd85cc 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -622,7 +622,7 @@ let add_inductive_class env sigma ind = let env = push_context ~strict:false (Univ.AUContext.repr univs) env in let env = push_rel_context ctx env in let inst = Univ.make_abstract_instance univs in - let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in + let ty = Inductive.type_of_inductive ((mind, oneind), inst) in let r = Inductive.relevance_of_inductive env ind in { cl_univs = univs; cl_impl = GlobRef.IndRef ind; |