diff options
| author | Gaëtan Gilbert | 2020-02-07 13:25:59 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-07 13:25:59 +0100 |
| commit | 633d9829d4e3678583c9e1ad161253fb53be1290 (patch) | |
| tree | 4c7edf5c090b369574b68d587787bac4b74d89ba /kernel/indTyping.ml | |
| parent | adf04f62d3ff5b0651cec2e8596ce3900d3af1eb (diff) | |
| parent | 22b3b961804bea2c8b56cbab9a0c4902bf45c56c (diff) | |
Merge PR #11528: Checker does not rely on Monomorphic fields
Reviewed-by: SkySkimmer
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 719eb276df..113ee787f2 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -274,7 +274,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 |