diff options
| -rw-r--r-- | kernel/environ.ml | 4 | ||||
| -rw-r--r-- | kernel/environ.mli | 4 | ||||
| -rw-r--r-- | kernel/vconv.ml | 16 |
3 files changed, 12 insertions, 12 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 77820a301e..5d49609f35 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -222,6 +222,10 @@ let lookup_constant kn env = let lookup_mind kn env = fst (Mindmap_env.find kn env.env_globals.env_inductives) +let mind_context env mind = + let mib = lookup_mind mind env in + Declareops.inductive_polymorphic_context mib + let lookup_mind_key kn env = Mindmap_env.find kn env.env_globals.env_inductives diff --git a/kernel/environ.mli b/kernel/environ.mli index 6d4d3b282b..4eb5f5d6d7 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -240,6 +240,10 @@ val add_mind : MutInd.t -> mutual_inductive_body -> env -> env raises [Not_found] if the required path is not found *) val lookup_mind : MutInd.t -> env -> mutual_inductive_body +(** The universe context associated to the inductive, empty if not + polymorphic *) +val mind_context : env -> MutInd.t -> Univ.AUContext.t + (** New-style polymorphism *) val polymorphic_ind : inductive -> env -> bool val polymorphic_pind : pinductive -> env -> bool diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 246c90c09d..08b0a6c926 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -86,17 +86,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); @@ -108,8 +102,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 |