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 /checker | |
| 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 'checker')
| -rw-r--r-- | checker/checkInductive.ml | 3 | ||||
| -rw-r--r-- | checker/values.ml | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index a2cf44389e..66d7e9cfee 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -69,8 +69,9 @@ let check_arity env ar1 ar2 = match ar1, ar2 with | RegularArity ar, RegularArity {mind_user_arity;mind_sort} -> Constr.equal ar.mind_user_arity mind_user_arity && Sorts.equal ar.mind_sort mind_sort - | TemplateArity ar, TemplateArity {template_param_levels;template_level} -> + | TemplateArity ar, TemplateArity {template_param_levels;template_level;template_context} -> List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels && + ContextSet.equal template_context ar.template_context && UGraph.check_leq (universes env) template_level ar.template_level (* template_level is inferred by indtypes, so functor application can produce a smaller one *) | (RegularArity _ | TemplateArity _), _ -> assert false diff --git a/checker/values.ml b/checker/values.ml index fff166f27b..c8bbc092b4 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -228,7 +228,7 @@ let v_oracle = |] let v_pol_arity = - v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] + v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ;v_context_set|] let v_primitive = v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *) |