From a9010048c40c85b0f5e9c5fedaf2609121e71b89 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 24 May 2016 20:32:35 +0200
Subject: primproj: warning and avoid error.

When defining a (co)recursive inductive with primitive projections on,
which lacks eta-conversion and hence dependent elimination, build only
the associated non-dependent elimination principles, and warn about
this. Also make the printing of the status of an inductive
w.r.t. projections and eta conversion explicit in Print and About.
---
 printing/prettyp.ml     |  8 ++++----
 tactics/elimschemes.ml  |  4 ++++
 tactics/elimschemes.mli |  2 ++
 toplevel/indschemes.ml  | 24 +++++++++++++++++++++---
 4 files changed, 31 insertions(+), 7 deletions(-)

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 1f6e99c7e7..f71719cb9a 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -224,12 +224,12 @@ let print_type_in_type ref =
 let print_primitive_record recflag mipv = function
   | Some (Some (_, ps,_)) ->
     let eta = match recflag with
-    | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt ()
-    | Decl_kinds.BiFinite -> str " and has eta conversion"
+    | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion"
+    | Decl_kinds.BiFinite -> str " with eta conversion"
     in
-    [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
+    [pr_id mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."]
   | _ -> []
-    
+
 let print_primitive ref =
   match ref with 
   | IndRef ind -> 
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index de28189023..99c2d82106 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -95,6 +95,10 @@ let rec_scheme_kind_from_prop =
   declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop"
   (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet)
 
+let rec_scheme_kind_from_type =
+  declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type"
+  (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet)
+
 let rec_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rec" ~aux:"_rec_from_type"
   (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet)
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index c36797059e..77f927f2df 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -13,9 +13,11 @@ open Ind_tables
 val rect_scheme_kind_from_prop : individual scheme_kind
 val ind_scheme_kind_from_prop : individual scheme_kind
 val rec_scheme_kind_from_prop : individual scheme_kind
+val rect_scheme_kind_from_type : individual scheme_kind
 val rect_dep_scheme_kind_from_type : individual scheme_kind
 val ind_scheme_kind_from_type : individual scheme_kind
 val ind_dep_scheme_kind_from_type : individual scheme_kind
+val rec_scheme_kind_from_type : individual scheme_kind
 val rec_dep_scheme_kind_from_type : individual scheme_kind
 
 
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 32e0eb53b0..8ae2140a6c 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -213,11 +213,20 @@ let try_declare_beq_scheme kn =
 
 let declare_beq_scheme = declare_beq_scheme_with []
 
+let is_primitive_record_without_eta mib =
+  match mib.mind_record with
+  | Some (Some _) -> mib.mind_finite <> BiFinite
+  | _ -> false
+
 (* Case analysis schemes *)
 let declare_one_case_analysis_scheme ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let kind = inductive_sort_family mip in
-  let dep = if kind == InProp then case_scheme_kind_from_prop else case_dep_scheme_kind_from_type in
+  let dep =
+    if kind == InProp then case_scheme_kind_from_prop
+    else if is_primitive_record_without_eta mib then
+      case_scheme_kind_from_type
+    else case_dep_scheme_kind_from_type in
   let kelim = elim_sorts (mib,mip) in
     (* in case the inductive has a type elimination, generates only one
        induction scheme, the other ones share the same code with the
@@ -237,15 +246,23 @@ let kinds_from_type =
    InProp,ind_dep_scheme_kind_from_type;
    InSet,rec_dep_scheme_kind_from_type]
 
+let nondep_kinds_from_type =
+  [InType,rect_scheme_kind_from_type;
+   InProp,ind_scheme_kind_from_type;
+   InSet,rec_scheme_kind_from_type]
+
 let declare_one_induction_scheme ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let kind = inductive_sort_family mip in
   let from_prop = kind == InProp in
+  let primwithouteta = is_primitive_record_without_eta mib in
   let kelim = elim_sorts (mib,mip) in
   let elims =
     List.map_filter (fun (sort,kind) ->
       if Sorts.List.mem sort kelim then Some kind else None)
-      (if from_prop then kinds_from_prop else kinds_from_type) in
+      (if from_prop then kinds_from_prop
+       else if primwithouteta then nondep_kinds_from_type
+       else kinds_from_type) in
   List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind))
     elims
 
@@ -502,7 +519,8 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done
 let declare_default_schemes kn =
   let mib = Global.lookup_mind kn in
   let n = Array.length mib.mind_packets in
-  if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) && mib.mind_typing_flags.check_guarded then
+  if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag)
+     && mib.mind_typing_flags.check_guarded then
     declare_induction_schemes kn;
   if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n;
   if is_eq_flag() then try_declare_beq_scheme kn;
-- 
cgit v1.2.3


From a7ed091b6842cc78f0480504e84c3cfa261860bd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 25 May 2016 13:38:51 +0200
Subject: Move is_prim... to Inductiveops and correct Scheme

Now scheme will not try to build ill-typed dependent analyses
on recursive records with primitive projections but report
a proper error.

Minor change of the API (adding one error case to recursion_scheme_error).
---
 pretyping/indrec.ml        |  9 ++++++++-
 pretyping/indrec.mli       |  7 +++++--
 pretyping/inductiveops.ml  |  5 +++++
 pretyping/inductiveops.mli |  5 ++++-
 toplevel/himsg.ml          |  7 +++++++
 toplevel/indschemes.ml     | 10 ++--------
 6 files changed, 31 insertions(+), 12 deletions(-)

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 0c80bd0193..012c975498 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -36,6 +36,7 @@ type dep_flag = bool
 type recursion_scheme_error =
   | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive
   | NotMutualInScheme of inductive * inductive
+  | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive
 
 exception RecursionSchemeError of recursion_scheme_error
 
@@ -483,6 +484,8 @@ let mis_make_indrec env sigma listdepkind mib u =
 
 let build_case_analysis_scheme env sigma pity dep kind =
   let (mib,mip) = lookup_mind_specif env (fst pity) in
+  if dep && Inductiveops.is_primitive_record_without_eta mib then
+    raise (RecursionSchemeError (NotAllowedDependentAnalysis (false, fst pity)));
   mis_make_case_com dep env sigma pity (mib,mip) kind
 
 let is_in_prop mip =
@@ -492,7 +495,7 @@ let is_in_prop mip =
 
 let build_case_analysis_scheme_default env sigma pity kind =
   let (mib,mip) = lookup_mind_specif env (fst pity) in
-  let dep = not (is_in_prop mip) in
+  let dep = not (is_in_prop mip || Inductiveops.is_primitive_record_without_eta mib) in
   mis_make_case_com dep env sigma pity (mib,mip) kind
 
 (**********************************************************************)
@@ -553,6 +556,8 @@ let check_arities env listdepkind =
 let build_mutual_induction_scheme env sigma = function
   | ((mind,u),dep,s)::lrecspec ->
       let (mib,mip) = lookup_mind_specif env mind in
+      if dep && Inductiveops.is_primitive_record_without_eta mib then
+        raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, mind)));
       let (sp,tyi) = mind in
       let listdepkind =
 	((mind,u),mib,mip,dep,s)::
@@ -572,6 +577,8 @@ let build_mutual_induction_scheme env sigma = function
 
 let build_induction_scheme env sigma pind dep kind =
   let (mib,mip) = lookup_mind_specif env (fst pind) in
+  if dep && Inductiveops.is_primitive_record_without_eta mib then
+    raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, fst pind)));
   let sigma, l = mis_make_indrec env sigma [(pind,mib,mip,dep,kind)] mib (snd pind) in
     sigma, List.hd l
 
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index f0736d2dda..192b64a5ed 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -16,6 +16,7 @@ open Evd
 type recursion_scheme_error =
   | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive
   | NotMutualInScheme of inductive * inductive
+  | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive
 
 exception RecursionSchemeError of recursion_scheme_error
 
@@ -28,13 +29,15 @@ type dep_flag = bool
 val build_case_analysis_scheme : env -> 'r Sigma.t -> pinductive ->
       dep_flag -> sorts_family -> (constr, 'r) Sigma.sigma
 
-(** Build a dependent case elimination predicate unless type is in Prop *)
+(** Build a dependent case elimination predicate unless type is in Prop
+   or is a recursive record with primitive projections. *)
 
 val build_case_analysis_scheme_default : env -> 'r Sigma.t -> pinductive ->
       sorts_family -> (constr, 'r) Sigma.sigma
 
 (** Builds a recursive induction scheme (Peano-induction style) in the same
-   sort family as the inductive family; it is dependent if not in Prop *)
+   sort family as the inductive family; it is dependent if not in Prop
+   or a recursive record with primitive projections.  *)
 
 val build_induction_scheme : env -> evar_map -> pinductive ->
       dep_flag -> sorts_family -> evar_map * constr
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index fbad0d949d..64932145e1 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -269,6 +269,11 @@ let projection_nparams_env env p =
 
 let projection_nparams p = projection_nparams_env (Global.env ()) p
 
+let is_primitive_record_without_eta mib =
+  match mib.mind_record with
+  | Some (Some _) -> mib.mind_finite <> Decl_kinds.BiFinite
+  | _ -> false
+
 (* Annotation for cases *)
 let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index d25f8a8378..6c49099a8f 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -126,7 +126,10 @@ val allowed_sorts : env -> inductive -> sorts_family list
 val projection_nparams : projection -> int
 val projection_nparams_env : env -> projection -> int
 val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
-  constr -> types -> types
+				     constr -> types -> types
+
+(** Recursive records with primitive projections do not have eta-conversion *)
+val is_primitive_record_without_eta : mutual_inductive_body -> bool
 
 (** Extract information from an inductive family *)
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 1e4c3c8f11..b3eae3765b 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1147,6 +1147,11 @@ let error_not_allowed_case_analysis isrec kind i =
   strbrk " is not allowed for inductive definition " ++
   pr_inductive (Global.env()) (fst i) ++ str "."
 
+let error_not_allowed_dependent_analysis isrec i =
+  str "Dependent " ++ str (if isrec then "Induction" else "Case analysis") ++
+  strbrk " is not allowed for inductive definition " ++
+  pr_inductive (Global.env()) i ++ str "."
+
 let error_not_mutual_in_scheme ind ind' =
   if eq_ind ind ind' then
     str "The inductive type " ++ pr_inductive (Global.env()) ind ++
@@ -1178,6 +1183,8 @@ let explain_recursion_scheme_error = function
   | NotAllowedCaseAnalysis (isrec,k,i) ->
       error_not_allowed_case_analysis isrec k i
   | NotMutualInScheme (ind,ind')-> error_not_mutual_in_scheme ind ind'
+  | NotAllowedDependentAnalysis (isrec, i) ->
+     error_not_allowed_dependent_analysis isrec i
 
 (* Pattern-matching errors *)
 
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 8ae2140a6c..ecee2e540c 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -213,18 +213,13 @@ let try_declare_beq_scheme kn =
 
 let declare_beq_scheme = declare_beq_scheme_with []
 
-let is_primitive_record_without_eta mib =
-  match mib.mind_record with
-  | Some (Some _) -> mib.mind_finite <> BiFinite
-  | _ -> false
-
 (* Case analysis schemes *)
 let declare_one_case_analysis_scheme ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let kind = inductive_sort_family mip in
   let dep =
     if kind == InProp then case_scheme_kind_from_prop
-    else if is_primitive_record_without_eta mib then
+    else if Inductiveops.is_primitive_record_without_eta mib then
       case_scheme_kind_from_type
     else case_dep_scheme_kind_from_type in
   let kelim = elim_sorts (mib,mip) in
@@ -255,7 +250,7 @@ let declare_one_induction_scheme ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let kind = inductive_sort_family mip in
   let from_prop = kind == InProp in
-  let primwithouteta = is_primitive_record_without_eta mib in
+  let primwithouteta = Inductiveops.is_primitive_record_without_eta mib in
   let kelim = elim_sorts (mib,mip) in
   let elims =
     List.map_filter (fun (sort,kind) ->
@@ -409,7 +404,6 @@ let do_mutual_induction_scheme lnamedepindsort =
   let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
   let declare decl fi lrecref =
     let decltype = Retyping.get_type_of env0 sigma decl in
-    (* let decltype = refresh_universes decltype in *)
     let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
     let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in
     ConstRef cst :: lrecref
-- 
cgit v1.2.3


From f77c2b488ca552b2316d4ebab1c051cb5a1347ab Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 25 May 2016 13:49:50 +0200
Subject: Renaming to more generic has_dependent_elim test

---
 pretyping/indrec.ml        | 8 ++++----
 pretyping/inductiveops.ml  | 6 +++---
 pretyping/inductiveops.mli | 6 ++++--
 toplevel/indschemes.ml     | 8 ++++----
 4 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 012c975498..45eaae1244 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -484,7 +484,7 @@ let mis_make_indrec env sigma listdepkind mib u =
 
 let build_case_analysis_scheme env sigma pity dep kind =
   let (mib,mip) = lookup_mind_specif env (fst pity) in
-  if dep && Inductiveops.is_primitive_record_without_eta mib then
+  if dep && not (Inductiveops.has_dependent_elim mib) then
     raise (RecursionSchemeError (NotAllowedDependentAnalysis (false, fst pity)));
   mis_make_case_com dep env sigma pity (mib,mip) kind
 
@@ -495,7 +495,7 @@ let is_in_prop mip =
 
 let build_case_analysis_scheme_default env sigma pity kind =
   let (mib,mip) = lookup_mind_specif env (fst pity) in
-  let dep = not (is_in_prop mip || Inductiveops.is_primitive_record_without_eta mib) in
+  let dep = not (is_in_prop mip || not (Inductiveops.has_dependent_elim mib)) in
   mis_make_case_com dep env sigma pity (mib,mip) kind
 
 (**********************************************************************)
@@ -556,7 +556,7 @@ let check_arities env listdepkind =
 let build_mutual_induction_scheme env sigma = function
   | ((mind,u),dep,s)::lrecspec ->
       let (mib,mip) = lookup_mind_specif env mind in
-      if dep && Inductiveops.is_primitive_record_without_eta mib then
+      if dep && not (Inductiveops.has_dependent_elim mib) then
         raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, mind)));
       let (sp,tyi) = mind in
       let listdepkind =
@@ -577,7 +577,7 @@ let build_mutual_induction_scheme env sigma = function
 
 let build_induction_scheme env sigma pind dep kind =
   let (mib,mip) = lookup_mind_specif env (fst pind) in
-  if dep && Inductiveops.is_primitive_record_without_eta mib then
+  if dep && not (Inductiveops.has_dependent_elim mib) then
     raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, fst pind)));
   let sigma, l = mis_make_indrec env sigma [(pind,mib,mip,dep,kind)] mib (snd pind) in
     sigma, List.hd l
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 64932145e1..e4f98e7301 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -269,10 +269,10 @@ let projection_nparams_env env p =
 
 let projection_nparams p = projection_nparams_env (Global.env ()) p
 
-let is_primitive_record_without_eta mib =
+let has_dependent_elim mib =
   match mib.mind_record with
-  | Some (Some _) -> mib.mind_finite <> Decl_kinds.BiFinite
-  | _ -> false
+  | Some (Some _) -> mib.mind_finite == Decl_kinds.BiFinite
+  | _ -> true
 
 (* Annotation for cases *)
 let make_case_info env ind style =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 6c49099a8f..7ef848f0de 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -122,14 +122,16 @@ val inductive_has_local_defs : inductive -> bool
 
 val allowed_sorts : env -> inductive -> sorts_family list
 
+(** (Co)Inductive records with primitive projections do not have eta-conversion,
+    hence no dependent elimination. *)
+val has_dependent_elim : mutual_inductive_body -> bool
+
 (** Primitive projections *)
 val projection_nparams : projection -> int
 val projection_nparams_env : env -> projection -> int
 val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
 				     constr -> types -> types
 
-(** Recursive records with primitive projections do not have eta-conversion *)
-val is_primitive_record_without_eta : mutual_inductive_body -> bool
 
 (** Extract information from an inductive family *)
 
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index ecee2e540c..f9e6c207c3 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -219,7 +219,7 @@ let declare_one_case_analysis_scheme ind =
   let kind = inductive_sort_family mip in
   let dep =
     if kind == InProp then case_scheme_kind_from_prop
-    else if Inductiveops.is_primitive_record_without_eta mib then
+    else if not (Inductiveops.has_dependent_elim mib) then
       case_scheme_kind_from_type
     else case_dep_scheme_kind_from_type in
   let kelim = elim_sorts (mib,mip) in
@@ -250,14 +250,14 @@ let declare_one_induction_scheme ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let kind = inductive_sort_family mip in
   let from_prop = kind == InProp in
-  let primwithouteta = Inductiveops.is_primitive_record_without_eta mib in
+  let depelim = Inductiveops.has_dependent_elim mib in
   let kelim = elim_sorts (mib,mip) in
   let elims =
     List.map_filter (fun (sort,kind) ->
       if Sorts.List.mem sort kelim then Some kind else None)
       (if from_prop then kinds_from_prop
-       else if primwithouteta then nondep_kinds_from_type
-       else kinds_from_type) in
+       else if depelim then kinds_from_type
+       else nondep_kinds_from_type) in
   List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind))
     elims
 
-- 
cgit v1.2.3


From f8a5cb590352a617de38fdd8ba5ffff7691d9841 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 25 May 2016 15:17:28 +0200
Subject: Disallow dependent case on prim records w/o eta

---
 pretyping/cases.ml                 | 12 +++---------
 pretyping/indrec.ml                | 25 ++++---------------------
 pretyping/inductiveops.ml          | 29 +++++++++++++++++++++++++++++
 pretyping/inductiveops.mli         |  8 ++++++++
 tactics/equality.ml                |  2 +-
 test-suite/success/primitiveproj.v |  2 ++
 6 files changed, 47 insertions(+), 31 deletions(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 985ad4b0d3..447a4c487c 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 45eaae1244..39aeb41f77 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 e4f98e7301..3fbed4b252 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 7ef848f0de..7bd616591f 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*)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f18de92c03..4aa7ffa7bd 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -860,7 +860,7 @@ let descend_then env sigma head dirn =
         List.map build_branch
           (List.interval 1 (Array.length mip.mind_consnames)) in
       let ci = make_case_info env ind RegularStyle in
-      mkCase (ci, p, head, Array.of_list brl)))
+      Inductiveops.make_case_or_project env indf ci p head (Array.of_list brl)))
 
 (* Now we need to construct the discriminator, given a discriminable
    position.  This boils down to:
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index b5e6ccd618..473d37eb36 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -47,7 +47,9 @@ Check _.(next) : option Y.
 Lemma eta_ind (y : Y) : y = Build_Y y.(next).
 Proof. Fail reflexivity. Abort.
 
+Record Fdef := { Fa : nat ; Fb := Fa; Fc : nat }.
 
+Scheme Fdef_rec := Induction for Fdef Sort Prop.
 
 (* 
   Rules for parsing and printing of primitive projections and their eta expansions.
-- 
cgit v1.2.3


From f46f4ecec94953930fca6bbbc9fdb83a7a1025fc Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 25 May 2016 15:24:22 +0200
Subject: Fixed bug #4622.

---
 test-suite/bugs/closed/4622.v      | 24 ++++++++++++++++++++++++
 test-suite/success/primitiveproj.v |  4 ++--
 2 files changed, 26 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/4622.v

diff --git a/test-suite/bugs/closed/4622.v b/test-suite/bugs/closed/4622.v
new file mode 100644
index 0000000000..ffa478cb87
--- /dev/null
+++ b/test-suite/bugs/closed/4622.v
@@ -0,0 +1,24 @@
+Set Primitive Projections.
+
+Record foo : Type := bar { x : unit }.
+
+Goal forall t u, bar t = bar u -> t = u.
+Proof.
+  intros.
+  injection H.
+  trivial.
+Qed.
+(* Was: Error: Pattern-matching expression on an object of inductive type foo has invalid information. *)
+
+(** Dependent pattern-matching is ok on this one as it has eta *)
+Definition baz (x : foo) :=
+  match x as x' return x' = x' with
+  | bar u => eq_refl
+  end.
+
+Inductive foo' : Type := bar' {x' : unit; y: foo'}.
+(** Dependent pattern-matching is not ok on this one *)
+Fail Definition baz' (x : foo') :=
+  match x as x' return x' = x' with
+  | bar' u y => eq_refl
+  end.
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 473d37eb36..2fa7704941 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -47,9 +47,9 @@ Check _.(next) : option Y.
 Lemma eta_ind (y : Y) : y = Build_Y y.(next).
 Proof. Fail reflexivity. Abort.
 
-Record Fdef := { Fa : nat ; Fb := Fa; Fc : nat }.
+Inductive Fdef := { Fa : nat ; Fb := Fa; Fc : Fdef }.
 
-Scheme Fdef_rec := Induction for Fdef Sort Prop.
+Fail Scheme Fdef_rec := Induction for Fdef Sort Prop.
 
 (* 
   Rules for parsing and printing of primitive projections and their eta expansions.
-- 
cgit v1.2.3


From df24a81b255190493281ffdeeef36754b076e9cd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 4 Jul 2016 14:36:31 +0200
Subject: Fix reopened bug #3317.

---
 pretyping/inductiveops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 3fbed4b252..214e19fecf 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -360,7 +360,7 @@ let make_case_or_project env indf ci pred c branches =
 		     str" on inductive type " ++ Names.MutInd.print (fst ind))
      in
      let branch = branches.(0) in
-     let ctx, br = decompose_lam_assum branch in
+     let ctx, br = decompose_lam_n_assum (Array.length ps) branch in
      let n, subst =
        List.fold_right
          (fun decl (i, subst) ->
-- 
cgit v1.2.3