Disallow dependent case on prim records w/o eta

4 files changed, 44 insertions, 30 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 985ad4b0d..447a4c487 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1329,14 +1329,6 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
 
 *)
 
-let mk_case pb (ci,pred,c,brs) =
-  let mib = lookup_mind (fst ci.ci_ind) pb.env in
-    match mib.mind_record with
-    | Some (Some (_, cs, pbs)) ->
-      Reduction.beta_appvect brs.(0) 
-	(Array.map (fun p -> mkProj (Projection.make p true, c)) cs)
-    | _ -> mkCase (ci,pred,c,brs)
-
 (**********************************************************************)
 (* Main compiling descent *)
 let rec compile pb =
@@ -1383,7 +1375,9 @@ and match_current pb (initial,tomatch) =
 	      pred current indt (names,dep) tomatch in
 	  let ci = make_case_info pb.env (fst mind) pb.casestyle in
 	  let pred = nf_betaiota !(pb.evdref) pred in
-	  let case = mk_case pb (ci,pred,current,brvals) in
+	  let case =
+	    make_case_or_project pb.env indf ci pred current brvals
+	  in
 	  Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
 	  { uj_val = applist (case, inst);
 	    uj_type = prod_applist typ inst }
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 45eaae124..39aeb41f7 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -43,6 +43,7 @@ exception RecursionSchemeError of recursion_scheme_error
 let make_prod_dep dep env = if dep then mkProd_name env else mkProd
 let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c)
 
+
 (*******************************************)
 (* Building curryfied elimination          *)
 (*******************************************)
@@ -376,27 +377,9 @@ let mis_make_indrec env sigma listdepkind mib u =
 		      (Anonymous,depind',concl))
 		  arsign'
 	      in
-	      let obj = 
-		let projs = get_projections env indf in
-		  match projs with
-		  | None -> (mkCase (ci, pred,
-				     mkRel 1,
-				     branches))
-		  | Some ps -> 
-		    let branch = branches.(0) in
-		    let ctx, br = decompose_lam_assum branch in
-		    let n, subst = 
-		      List.fold_right (fun decl (i, subst) ->
-			match decl with
-			| LocalAssum (na,t) ->
-			    let t = mkProj (Projection.make ps.(i) true, mkRel 1) in
-			    i + 1, t :: subst
-			| LocalDef (na,b,t) ->
-			    i, mkRel 0 :: subst)
-			ctx (0, [])
-		    in
-		    let term = substl subst br in
-		      term
+	      let obj =
+		Inductiveops.make_case_or_project env indf ci pred
+						  (mkRel 1) branches
 	      in
 		it_mkLambda_or_LetIn_name env obj
 		  (Termops.lift_rel_context nrec deparsign)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index e4f98e730..3fbed4b25 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -343,6 +343,35 @@ let get_projections env (ind,params) =
     | Some (Some (id, projs, pbs)) -> Some projs
     | _ -> None
 
+let make_case_or_project env indf ci pred c branches =
+  let projs = get_projections env indf in
+  match projs with
+  | None -> (mkCase (ci, pred, c, branches))
+  | Some ps ->
+     assert(Array.length branches == 1);
+     let () =
+       let _, _, t = destLambda pred in
+       let (ind, _), _ = dest_ind_family indf in
+       let mib, _ = Inductive.lookup_mind_specif env ind in
+       if (* dependent *) not (noccurn 1 t) &&
+          not (has_dependent_elim mib) then
+       errorlabstrm "make_case_or_project"
+		    Pp.(str"Dependent case analysis not allowed" ++
+		     str" on inductive type " ++ Names.MutInd.print (fst ind))
+     in
+     let branch = branches.(0) in
+     let ctx, br = decompose_lam_assum branch in
+     let n, subst =
+       List.fold_right
+         (fun decl (i, subst) ->
+	  match decl with
+	  | LocalAssum (na, t) ->
+	     let t = mkProj (Projection.make ps.(i) true, c) in
+	     (i + 1, t :: subst)
+	  | LocalDef (na, b, t) -> (i, substl subst b :: subst))
+	 ctx (0, [])
+     in substl subst br
+
 (* substitution in a signature *)
 
 let substnl_rel_context subst n sign =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 7ef848f0d..7bd616591 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -180,6 +180,14 @@ val type_case_branches_with_names :
 (** Annotation for cases *)
 val make_case_info : env -> inductive -> case_style -> case_info
 
+(** Make a case or substitute projections if the inductive type is a record
+    with primitive projections.
+    Fail with an error if the elimination is dependent while the
+    inductive type does not allow dependent elimination. *)
+val make_case_or_project :
+  env -> inductive_family -> case_info ->
+  (* pred *) constr -> (* term *) constr -> (* branches *) constr array -> constr
+
 (*i Compatibility
 val make_default_case_info : env -> case_style -> inductive -> case_info
 i*)