Change the way primitive projections are declared to the kernel.

Now kernel/indtypes builds the corresponding terms (has to be trusted)
while translate_constant just binds a constant name to the
already entered projection body, avoiding the dubious "check"
of user given terms. "case" Pattern-matching on primitive records is
now disallowed, and the default scheme is implemented using
projections and eta (all elimination tactics now use projections
as well). Elaborate "let (x, y) := p in t" using let bindings
for the projections of p too.

8 files changed, 83 insertions, 37 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 04c69d74ae..627a954f9d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -760,7 +760,7 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1),
 and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
-    | Some (exp,projs) when Array.length projs > 0
+    | Some (projs, pbs) when Array.length projs > 0
       && mib.Declarations.mind_finite -> 
       let pars = mib.Declarations.mind_nparams in
 	(try 
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 81b5c9ad83..547268ef08 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -60,7 +60,11 @@ let check_privacy_block mib =
 
 let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
   let lnamespar = Vars.subst_instance_context u mib.mind_params_ctxt in
-  let () = check_privacy_block mib in
+  let indf = make_ind_family(pind, Termops.extended_rel_list 0 lnamespar) in
+  let constrs = get_constructors env indf in
+  let projs = get_projections env indf in
+
+  let () = if Option.is_empty projs then check_privacy_block mib in
   let () = 
     if not (Sorts.List.mem kind (elim_sorts specif)) then
       raise
@@ -73,8 +77,6 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
   (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
   let env' = push_rel_context lnamespar env in
 
-  let indf = make_ind_family(pind, Termops.extended_rel_list 0 lnamespar) in
-  let constrs = get_constructors env indf in
 
   let rec add_branch env k =
     if Int.equal k (Array.length mip.mind_consnames) then
@@ -97,11 +99,16 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
 	   (Anonymous,depind,pbody))
           arsign
       in
-      it_mkLambda_or_LetIn_name env'
-       	(mkCase (ci, lift ndepar p,
-		     mkRel 1,
-		     Termops.rel_vect ndepar k))
-       	deparsign
+      let obj = 
+	match projs with
+	| None -> mkCase (ci, lift ndepar p,  mkRel 1,
+			  Termops.rel_vect ndepar k)
+	| Some ps -> 
+	  let term = mkApp (mkRel 2, Array.map (fun p -> mkProj (p, mkRel 1)) ps) in
+	  let ty = mkApp (mkRel 3, [| mkRel 1 |]) in
+	    mkCast (term, DEFAULTcast, ty)
+      in
+	it_mkLambda_or_LetIn_name env' obj deparsign
     else
       let cs = lift_constructor (k+1) constrs.(k) in
       let t = build_branch_type env dep (mkRel (k+1)) cs in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 34243f499c..913afb2191 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -331,6 +331,12 @@ let get_constructors env (ind,params) =
   Array.init (Array.length mip.mind_consnames)
     (fun j -> get_constructor (ind,mib,mip,params) (j+1))
 
+let get_projections env (ind,params) =
+  let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
+    match mib.mind_record with
+    | Some (projs, pbs) when Array.length projs > 0 -> Some projs
+    | _ -> None
+
 (* substitution in a signature *)
 
 let substnl_rel_context subst n sign =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 03d41015bb..124f3a34e4 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -140,6 +140,8 @@ val get_constructor :
   int -> constructor_summary
 val get_arity        : env -> inductive_family -> rel_context * sorts_family
 val get_constructors : env -> inductive_family -> constructor_summary array
+val get_projections  : env -> inductive_family -> constant array option
+
 val build_dependent_constructor : constructor_summary -> constr
 val build_dependent_inductive   : env -> inductive_family -> constr
 val make_arity_signature : env -> bool -> inductive_family -> rel_context
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index cb3e81efea..56a6671152 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -678,25 +678,46 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	  error_case_not_inductive_loc cloc env !evdref cj
     in
     let cstrs = get_constructors env indf in
-      if not (Int.equal (Array.length cstrs) 1) then
-        user_err_loc (loc,"",str "Destructing let is only for inductive types" ++
-	  str " with one constructor.");
-      let cs = cstrs.(0) in
-	if not (Int.equal (List.length nal) cs.cs_nargs) then
-          user_err_loc (loc,"", str "Destructing let on this type expects " ++ 
-	    int cs.cs_nargs ++ str " variables.");
-	let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
-          (List.rev nal) cs.cs_args in
-	let env_f = push_rel_context fsign env in
-	  (* Make dependencies from arity signature impossible *)
-	let arsgn =
-	  let arsgn,_ = get_arity env indf in
-	    if not !allow_anonymous_refs then
-	      List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
-	    else arsgn
-	in
-	let psign = (na,None,build_dependent_inductive env indf)::arsgn in
-	let nar = List.length arsgn in
+    if not (Int.equal (Array.length cstrs) 1) then
+      user_err_loc (loc,"",str "Destructing let is only for inductive types" ++
+	str " with one constructor.");
+    let cs = cstrs.(0) in
+    if not (Int.equal (List.length nal) cs.cs_nargs) then
+      user_err_loc (loc,"", str "Destructing let on this type expects " ++ 
+	int cs.cs_nargs ++ str " variables.");
+    let fsign, record = 
+      match get_projections env indf with
+      | None -> List.map2 (fun na (_,c,t) -> (na,c,t))
+	(List.rev nal) cs.cs_args, false
+      | Some ps ->
+	let rec aux n k names l =
+	  match names, l with
+	  | na :: names, ((_, None, t) :: l) -> 
+	    (na, Some (lift (cs.cs_nargs - n) (mkProj (ps.(cs.cs_nargs - k), cj.uj_val))), t)
+	    :: aux (n+1) (k + 1) names l
+	  | na :: names, ((_, c, t) :: l) -> 
+	    (na, c, t) :: aux (n+1) k names l
+	  | [], [] -> []
+	  | _ -> assert false
+	in aux 1 1 (List.rev nal) cs.cs_args, true
+    in
+    let obj ind p v f =
+      if not record then 
+	let f = it_mkLambda_or_LetIn f fsign in
+	let ci = make_case_info env (fst ind) LetStyle in
+	  mkCase (ci, p, cj.uj_val,[|f|]) 
+      else it_mkLambda_or_LetIn f fsign
+    in
+    let env_f = push_rel_context fsign env in
+      (* Make dependencies from arity signature impossible *)
+    let arsgn =
+      let arsgn,_ = get_arity env indf in
+	if not !allow_anonymous_refs then
+	  List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
+	else arsgn
+    in
+      let psign = (na,None,build_dependent_inductive env indf)::arsgn in
+      let nar = List.length arsgn in
 	  (match po with
 	  | Some p ->
 	    let env_p = push_rel_context psign env in
@@ -710,18 +731,16 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	    let lp = lift cs.cs_nargs p in
 	    let fty = hnf_lam_applist env !evdref lp inst in
 	    let fj = pretype (mk_tycon fty) env_f evdref lvar d in
-	    let f = it_mkLambda_or_LetIn fj.uj_val fsign in
 	    let v =
 	      let ind,_ = dest_ind_family indf in
-	      let ci = make_case_info env (fst ind) LetStyle in
 		Typing.check_allowed_sort env !evdref ind cj.uj_val p;
-		mkCase (ci, p, cj.uj_val,[|f|]) in
+		obj ind p cj.uj_val fj.uj_val
+	    in
 	      { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
 
 	  | None ->
 	    let tycon = lift_tycon cs.cs_nargs tycon in
 	    let fj = pretype tycon env_f evdref lvar d in
-	    let f = it_mkLambda_or_LetIn fj.uj_val fsign in
 	    let ccl = nf_evar !evdref fj.uj_type in
 	    let ccl =
 	      if noccur_between 1 cs.cs_nargs ccl then
@@ -733,9 +752,8 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	    let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
 	    let v =
 	      let ind,_ = dest_ind_family indf in
-	      let ci = make_case_info env (fst ind) LetStyle in
 		Typing.check_allowed_sort env !evdref ind cj.uj_val p;
-		mkCase (ci, p, cj.uj_val,[|f|])
+		obj ind p cj.uj_val fj.uj_val
 	    in { uj_val = v; uj_type = ccl })
 
   | GIf (loc,c,(na,po),b1,b2) ->
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index a2791f7a20..d1ab5b15de 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1110,9 +1110,18 @@ let pattern_occs loccs_trm env sigma c =
 (* Used in several tactics. *)
 
 let check_privacy env ind =
-  if (fst (Inductive.lookup_mind_specif env (fst ind))).Declarations.mind_private = Some true then
-    errorlabstrm "" (str "case analysis on a private type")
+  let spec = Inductive.lookup_mind_specif env (fst ind) in
+  if Inductive.is_private spec then
+    errorlabstrm "" (str "case analysis on a private type.")
   else ind
+
+let check_not_primitive_record env ind =
+  let spec = Inductive.lookup_mind_specif env (fst ind) in
+    if Inductive.is_primitive_record spec then
+      errorlabstrm "" (str "case analysis on a primitive record type: " ++
+		       str "use projections or let instead.")
+    else ind
+
 (* put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name
    return name, B and t' *)
 
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 91364c4aec..6d12d5d44c 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -103,3 +103,7 @@ val e_contextually : bool -> occurrences * constr_pattern ->
 (** Returns the same inductive if it is allowed for pattern-matching
     raises an error otherwise. **)
 val check_privacy : env -> inductive puniverses -> inductive puniverses
+
+(** Returns the same inductive if it is not a primitive record
+    raises an error otherwise. **)
+val check_not_primitive_record : env -> inductive puniverses -> inductive puniverses
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index aee7be9816..46f65271f4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -471,7 +471,7 @@ let eta_constructor_app env f l1 term =
   | Construct (((_, i as ind), j), u) ->
     let mib = lookup_mind (fst ind) env in
       (match mib.Declarations.mind_record with
-      | Some (exp,projs) ->
+      | Some (projs, _) ->
         let pars = mib.Declarations.mind_nparams in
 	let l1' = Array.sub l1 pars (Array.length l1 - pars) in
 	let l2 = Array.map (fun p -> mkProj (p, term)) projs in