diff options
| author | Matthieu Sozeau | 2014-10-11 12:11:07 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-11 12:15:49 +0200 |
| commit | d4b3de96f524887013c0955bd5b90f0311f086e6 (patch) | |
| tree | ea87e31c9c4681911c9dede29de2d1b51a86deec /kernel/indtypes.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/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 73a23ef059..39455a7d2a 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -661,7 +661,7 @@ exception UndefinableExpansion build an expansion function. The term built is expecting to be substituted first by a substitution of the form [params, x : ind params] *) -let compute_projections ((kn, _ as ind), u as indsp) n nparamargs params +let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params mind_consnrealdecls mind_consnrealargs ctx = let mp, dp, l = repr_mind kn in let rp = mkApp (mkIndU indsp, rel_vect 0 nparamargs) in @@ -674,7 +674,7 @@ let compute_projections ((kn, _ as ind), u as indsp) n nparamargs params ci_pp_info = print_info } in let len = List.length ctx in - let x = Name (Id.of_string (Unicode.lowercase_first_char (Id.to_string n))) in + let x = Name x in let compat_body ccl i = (* [ccl] is defined in context [params;x:rp] *) (* [ccl'] is defined in context [params;x:rp;x:rp] *) @@ -780,7 +780,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re let pkt = packets.(0) in let isrecord = match isrecord with - | Some true when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 -> + | Some (Some rid) when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 -> (** The elimination criterion ensures that all projections can be defined. *) let u = if p then @@ -792,11 +792,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re (try let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in let kns, projs = - compute_projections indsp pkt.mind_typename nparamargs params + compute_projections indsp pkt.mind_typename rid nparamargs params pkt.mind_consnrealdecls pkt.mind_consnrealargs fields - in Some (kns, projs) - with UndefinableExpansion -> Some ([||], [||])) - | Some _ -> Some ([||], [||]) + in Some (Some (rid, kns, projs)) + with UndefinableExpansion -> Some None) + | Some _ -> Some None | None -> None in (* Build the mutual inductive *) |