diff options
| author | Pierre-Marie Pédrot | 2020-02-05 15:39:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-05 17:00:04 +0100 |
| commit | 5f508021585c3b385e603524b49a25ecc65cfa7d (patch) | |
| tree | c190c6b509b411a1aee3e030871acbe58469805e /kernel/indTyping.ml | |
| parent | 2e273828c23fc50d924b1f3c3006fb2e9dc7d05b (diff) | |
Store the template polymorphic context inside the TemplateArity node.
This was the only part in the kernel that really relied on the contents
of the Monomorphic node.
Diffstat (limited to 'kernel/indTyping.ml')
| -rw-r--r-- | kernel/indTyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 591cd050a5..d5d5ec61bf 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -270,7 +270,7 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp CErrors.user_err Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") else - TemplateArity {template_param_levels = param_levels; template_level = min_univ} + TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx } in let kelim = allowed_sorts univ_info in |