1 files changed, 39 insertions, 45 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 14f2a3d8f..5d45c2c1a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -120,16 +120,6 @@ let mind_check_names mie =
 
 (* Typing the arities and constructor types *)
 
-(* An inductive definition is a "unit" if it has only one constructor
-   and that all arguments expected by this constructor are
-   logical, this is the case for equality, conjunction of logical properties
-*)
-let is_unit constrsinfos =
-  match constrsinfos with  (* One info = One constructor *)
-   | [level] -> is_type0m_univ level
-   | [] -> (* type without constructors *) true
-   | _ -> false
-
 let infos_and_sort env t =
   let rec aux env t max =
     let t = whd_all env t in
@@ -174,10 +164,9 @@ let infer_constructor_packet env_ar_par params lc =
   let lc'' = Array.map (fun j -> Term.it_mkProd_or_LetIn j.utj_val params) jlc in
   (* compute the max of the sorts of the products of the constructors types *)
   let levels = List.map (infos_and_sort env_ar_par) lc in
-  let isunit = is_unit levels in
   let min = if Array.length jlc > 1 then Universe.type0 else Universe.type0m in
   let level = List.fold_left (fun max l -> Universe.sup max l) min levels in
-  (lc'', (isunit, level))
+  (lc'', level)
 
 (* If indices matter *)
 let cumulate_arity_large_levels env sign =
@@ -354,7 +343,7 @@ let typecheck_inductive env mie =
   (* Compute/check the sorts of the inductive types *)
 
   let inds =
-    Array.map (fun ((id,full_arity,sign,expltype,def_level,inf_level),cn,lc,(is_unit,clev))  ->
+    Array.map (fun ((id,full_arity,sign,expltype,def_level,inf_level),cn,lc,clev)  ->
       let infu = 
 	(** Inferred level, with parameters and constructors. *)
 	match inf_level with
@@ -425,7 +414,7 @@ let typecheck_inductive env mie =
 type ill_formed_ind =
   | LocalNonPos of int
   | LocalNotEnoughArgs of int
-  | LocalNotConstructor of Context.Rel.t * int
+  | LocalNotConstructor of Constr.rel_context * int
   | LocalNonPar of int * int * int
 
 exception IllFormedInd of ill_formed_ind
@@ -797,15 +786,23 @@ 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) nparamargs params
-    mind_consnrealdecls mind_consnrealargs paramslet ctx =
+let compute_projections (kn, i as ind) mib =
+  let pkt = mib.mind_packets.(i) in
+  let u = match mib.mind_universes with
+  | Monomorphic_ind _ -> Univ.Instance.empty
+  | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx
+  | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi)
+  in
+  let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in
+  let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in
+  let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
   let mp, dp, l = MutInd.repr3 kn in
   (** We build a substitution smashing the lets in the record parameters so
       that typechecking projections requires just a substitution and not
       matching with a parameter context. *)
   let paramsletsubst =
     (* [Ind inst] is typed in context [params-wo-let] *)
-    let inst' = rel_list 0 nparamargs in
+    let inst' = rel_list 0 mib.mind_nparams in
     (* {params-wo-let |- subst:params] *)
     let subst = subst_of_rel_context_instance paramslet inst' in
     (* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *)
@@ -839,7 +836,7 @@ let compute_projections ((kn, _ as ind), u) nparamargs params
         (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
            to [params, x:I |- t(proj1 x,..,projj x)] *)
 	let fterm = mkProj (Projection.make kn false, mkRel 1) in
-	let body = { proj_ind = fst ind; proj_npars = nparamargs;
+        let body = { proj_ind = ind; proj_npars = mib.mind_nparams;
                       proj_arg = i; proj_type = projty; } in
         (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst)
       | Anonymous -> raise UndefinableExpansion
@@ -932,33 +929,9 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
 	mind_reloc_tbl = rtbl;
       } in
   let packets = Array.map2 build_one_packet inds recargs in
-  let pkt = packets.(0) in
-  let isrecord = 
-    match isrecord with
-    | Some (Some rid) when pkt.mind_kelim == all_sorts
-			   && Array.length pkt.mind_consnames == 1
-			   && pkt.mind_consnrealargs.(0) > 0 ->
-      (** The elimination criterion ensures that all projections can be defined. *)
-      let u =
-        match aiu with
-        | Monomorphic_ind _ -> Univ.Instance.empty
-        | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx
-        | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi)
-      in
-      let indsp = ((kn, 0), u) in
-      let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
-	(try 
-	   let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
-	   let kns, projs = 
-             compute_projections indsp nparamargs paramsctxt
-	       pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields
-	   in Some (Some (rid, kns, projs))
-	 with UndefinableExpansion -> Some None)
-    | Some _ -> Some None
-    | None -> None
-  in
-    (* Build the mutual inductive *)
-    { mind_record = isrecord;
+  let mib =
+      (* Build the mutual inductive *)
+    { mind_record = NotRecord;
       mind_ntypes = ntypes;
       mind_finite = isfinite;
       mind_hyps = hyps;
@@ -970,6 +943,27 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
       mind_private = prv;
       mind_typing_flags = Environ.typing_flags env;
     }
+  in
+  let record_info = match isrecord with
+  | Some (Some rid) ->
+    let is_record pkt =
+      pkt.mind_kelim == all_sorts
+      && Array.length pkt.mind_consnames == 1
+      && pkt.mind_consnrealargs.(0) > 0
+    in
+    (** The elimination criterion ensures that all projections can be defined. *)
+    if Array.for_all is_record packets then
+      let map i id =
+        let kn, projs = compute_projections (kn, i) mib in
+        (id, kn, projs)
+      in
+      try PrimRecord (Array.mapi map rid)
+      with UndefinableExpansion -> FakeRecord
+    else FakeRecord
+  | Some None -> FakeRecord
+  | None -> NotRecord
+  in
+  { mib with mind_record = record_info }
 
 (************************************************************************)
 (************************************************************************)