diff options
| author | Pierre-Marie Pédrot | 2019-02-05 15:53:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-05 15:53:55 +0100 |
| commit | 38b1682ee6b6342ca582bac4e658f7d1c3919de4 (patch) | |
| tree | c22a2690095ed66a086ebf6848e039c4ef4b7620 /kernel/vconv.ml | |
| parent | 9d3394cbc37be3ad8b4fbd32d32c193a55368196 (diff) | |
| parent | f7148d56b17ee7d06cac26392c85f3b8c7cbd974 (diff) | |
Merge PR #9438: Cleanup universe length for inductives in vconv
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/vconv.ml')
| -rw-r--r-- | kernel/vconv.ml | 16 |
1 files changed, 4 insertions, 12 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 04a17f7b08..414c443c4e 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -88,17 +88,11 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = match a1, a2 with | Aind ((mi,_i) as ind1) , Aind ind2 -> if eq_ind ind1 ind2 && compare_stack stk1 stk2 then - if Environ.polymorphic_ind ind1 env then - let mib = Environ.lookup_mind mi env in - let ulen = - match mib.Declarations.mind_universes with - | Declarations.Monomorphic_ind ctx -> Univ.ContextSet.size ctx - | Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx - | Declarations.Cumulative_ind cumi -> - Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) - in + let ulen = Univ.AUContext.size (Environ.mind_context env mi) in + if ulen = 0 then + conv_stack env k stk1 stk2 cu + else match stk1 , stk2 with - | [], [] -> assert (Int.equal ulen 0); cu | Zapp args1 :: stk1' , Zapp args2 :: stk2' -> assert (ulen <= nargs args1); assert (ulen <= nargs args2); @@ -110,8 +104,6 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = conv_arguments env ~from:ulen k args1 args2 (conv_stack env k stk1' stk2' cu) | _, _ -> assert false (* Should not happen if problem is well typed *) - else - conv_stack env k stk1 stk2 cu else raise NotConvertible | Aid ik1, Aid ik2 -> if Vmvalues.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then |