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 /library | |
| 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 'library')
| -rw-r--r-- | library/declare.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/declare.ml b/library/declare.ml index 8ec52d16a..1c9e10a19 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -382,7 +382,7 @@ let inInductive : inductive_obj -> obj = let declare_projections mind = let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in match spec.mind_record with - | Some (kns, pjs) -> + | Some (Some (_, kns, pjs)) -> Array.iteri (fun i kn -> let id = Label.to_id (Constant.label kn) in let entry = {proj_entry_ind = mind; proj_entry_arg = i} in @@ -390,7 +390,7 @@ let declare_projections mind = IsDefinition StructureComponent) in assert(eq_constant kn kn')) kns - | None -> () + | Some None | None -> () (* for initial declaration *) let declare_mind isrecord mie = |