diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 4 | ||||
| -rw-r--r-- | kernel/environ.mli | 4 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 10 | ||||
| -rw-r--r-- | kernel/vconv.ml | 16 |
4 files changed, 19 insertions, 15 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 02f38e7214..886d6b1feb 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 8d5bd85b94..a9e0717559 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -246,6 +246,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/indtypes.ml b/kernel/indtypes.ml index 9bb848c6a4..674d7a2a91 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -536,9 +536,13 @@ let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr let record_info = match isrecord with | Some (Some rid) -> let is_record pkt = - List.exists (Sorts.family_equal Sorts.InType) pkt.mind_kelim - && Array.length pkt.mind_consnames == 1 - && pkt.mind_consnrealargs.(0) > 0 + if Array.length pkt.mind_consnames != 1 then + user_err ~hdr:"build_inductive" + Pp.(str "Primitive records must have exactly one constructor.") + else if pkt.mind_consnrealargs.(0) = 0 then + user_err ~hdr:"build_inductive" + Pp.(str "Primitive records must have at least one constructor argument.") + else List.exists (Sorts.family_equal Sorts.InType) pkt.mind_kelim in (** The elimination criterion ensures that all projections can be defined. *) if Array.for_all is_record packets then 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 |