diff options
| author | Pierre-Marie Pédrot | 2020-03-06 10:57:19 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-08 15:31:27 +0100 |
| commit | e0bcbccf437ebee4157fdfdd5cba7b42019ead27 (patch) | |
| tree | be68f0664931c850ac09bb29575210f4c890a9bc /checker/values.ml | |
| parent | 4481b95f6f89acd7013b16a345d379dc44d67705 (diff) | |
Ensure that template parameters are shared in the same inductive block.
This could have been at the root of strange behaviours (read unsoundness).
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/checker/values.ml b/checker/values.ml index ed730cff8e..cba96e6636 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -227,8 +227,11 @@ let v_oracle = v_pred v_cst; |] -let v_pol_arity = - v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ;v_context_set|] +let v_template_arity = + v_tuple "template_arity" [|v_univ|] + +let v_template_universes = + v_tuple "template_universes" [|List(Opt v_level);v_context_set|] let v_primitive = v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *) @@ -265,7 +268,7 @@ let v_mono_ind_arity = v_tuple "monomorphic_inductive_arity" [|v_constr;v_sort|] let v_ind_arity = v_sum "inductive_arity" 0 - [|[|v_mono_ind_arity|];[|v_pol_arity|]|] + [|[|v_mono_ind_arity|];[|v_template_arity|]|] let v_one_ind = v_tuple "one_inductive_body" [|v_id; @@ -301,6 +304,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body" Int; v_rctxt; v_univs; (* universes *) + Opt v_template_universes; Opt (Array v_variance); Opt (Array v_variance); Opt v_bool; |