diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-11 12:11:07 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-11 12:15:49 +0200 |
| commit | d4b3de96f524887013c0955bd5b90f0311f086e6 (patch) | |
| tree | ea87e31c9c4681911c9dede29de2d1b51a86deec /kernel/term_typing.ml | |
| parent | d65496f09c4b68fa318783e53f9cd6d5c18e1eb7 (diff) | |
Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name
for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index a3c4d9849..232508bc8 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -169,11 +169,11 @@ let infer_declaration env kn dcl = let mib, _ = Inductive.lookup_mind_specif env (ind,0) in let kn, pb = match mib.mind_record with - | Some (kns, pbs) -> + | Some (Some (id, kns, pbs)) -> if i < Array.length pbs then kns.(i), pbs.(i) else assert false - | None -> assert false + | _ -> assert false in let term, typ = pb.proj_eta in Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb, |