From a5b631f7260e7d29defd8bd5c67db543742c9ecd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 9 May 2016 17:40:04 +0200
Subject: congruence/univs: properly refresh (fix #4609)

In congruence, refresh universes including the Set/Prop ones so that
congruence works with cumulativity, not restricting itself to the
inferred types of terms that are manipulated but allowing them to be
used at more general types. This fixes bug #4609.
---
 pretyping/evarsolve.ml  | 7 ++++++-
 pretyping/evarsolve.mli | 8 ++++++--
 2 files changed, 12 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 29af199a1e..c2d47790d5 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -47,7 +47,8 @@ let refresh_level evd s =
   | None -> true
   | Some l -> not (Evd.is_flexible_level evd l)
 
-let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t =
+let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(propset=false)
+		      pbty env evd t =
   let evdref = ref evd in
   let modified = ref false in
   let rec refresh status dir t = 
@@ -62,6 +63,10 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t =
       else set_leq_sort env !evdref s s'
     in
       modified := true; evdref := evd; mkSort s'
+    | Sort (Prop _ as s) when propset && not dir ->
+       let s' = evd_comb0 (new_sort_variable status) evdref in
+       let evd = set_leq_sort env !evdref s s' in
+       modified := true; evdref := evd; mkSort s'
     | Prod (na,u,v) -> 
       mkProd (na,u,refresh status dir v)
     | _ -> t
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 918ba12f0f..9ee815ebc0 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -34,8 +34,12 @@ type conv_fun_bool =
 val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> 
   bool option -> existential -> constr -> evar_map
 
-val refresh_universes : ?status:Evd.rigid ->
-			?onlyalg:bool (* Only algebraic universes *) ->
+val refresh_universes :
+  ?status:Evd.rigid ->
+  ?onlyalg:bool (* Only algebraic universes *) ->
+  ?propset:bool ->
+  (* Also refresh Prop and Set universes, so that the returned type can be any supertype
+     of the original type *)
   bool option (* direction: true for levels lower than the existing levels *) ->
   env -> evar_map -> types -> evar_map * types
 
-- 
cgit v1.2.3


From 71d4c435e42c24c21ae43f0ddcc7a71bee1009f5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 9 May 2016 18:31:01 +0200
Subject: congruence: Restrict refreshing to Set

Because refreshing Prop is not semantics-preserving,
the new universe is >= Set, so cannot be minimized to Prop
afterwards.
---
 pretyping/evarsolve.ml  | 4 ++--
 pretyping/evarsolve.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index c2d47790d5..0db309f948 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -47,7 +47,7 @@ let refresh_level evd s =
   | None -> true
   | Some l -> not (Evd.is_flexible_level evd l)
 
-let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(propset=false)
+let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 		      pbty env evd t =
   let evdref = ref evd in
   let modified = ref false in
@@ -63,7 +63,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(propset=false)
       else set_leq_sort env !evdref s s'
     in
       modified := true; evdref := evd; mkSort s'
-    | Sort (Prop _ as s) when propset && not dir ->
+    | Sort (Prop Pos as s) when refreshset && not dir ->
        let s' = evd_comb0 (new_sort_variable status) evdref in
        let evd = set_leq_sort env !evdref s s' in
        modified := true; evdref := evd; mkSort s'
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 9ee815ebc0..f94c83b6dc 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -37,7 +37,7 @@ val evar_define : conv_fun -> ?choose:bool -> env -> evar_map ->
 val refresh_universes :
   ?status:Evd.rigid ->
   ?onlyalg:bool (* Only algebraic universes *) ->
-  ?propset:bool ->
+  ?refreshset:bool ->
   (* Also refresh Prop and Set universes, so that the returned type can be any supertype
      of the original type *)
   bool option (* direction: true for levels lower than the existing levels *) ->
-- 
cgit v1.2.3


From 4a8c1e387bb0b971e651458319e77603d87b2d08 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 6 Jul 2016 10:46:29 +0200
Subject: Univs: fix internalization of (x := T) and casts

They were allowing algebraic universes to slip in terms.
---
 pretyping/pretyping.ml | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c8f61c66b8..187eba16b6 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -953,14 +953,17 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
       | CastConv t | CastVM t | CastNative t ->
 	let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in
 	let tj = pretype_type empty_valcon env evdref lvar t in
-	let tval = nf_evar !evdref tj.utj_val in
-	let cj = match k with
+        let tval = evd_comb1 (Evarsolve.refresh_universes
+                             ~onlyalg:true ~status:Evd.univ_flexible (Some false) env)
+                          evdref tj.utj_val in
+	let tval = nf_evar !evdref tval in
+	let cj, tval = match k with
 	  | VMcast ->
  	    let cj = pretype empty_tycon env evdref lvar c in
-	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
+	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
 	      if not (occur_existential cty || occur_existential tval) then
 		let (evd,b) = Reductionops.vm_infer_conv env !evdref cty tval in
-		if b then (evdref := evd; cj)
+		if b then (evdref := evd; cj, tval)
 		else
 		  error_actual_type_loc loc env !evdref cj tval 
                       (ConversionFailed (env,cty,tval))
@@ -968,16 +971,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 		str "unresolved arguments remain.")
 	  | NATIVEcast ->
  	    let cj = pretype empty_tycon env evdref lvar c in
-	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
+	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
             begin
 	      let (evd,b) = Nativenorm.native_infer_conv env !evdref cty tval in
-	      if b then (evdref := evd; cj)
+	      if b then (evdref := evd; cj, tval)
 	      else
                 error_actual_type_loc loc env !evdref cj tval 
                   (ConversionFailed (env,cty,tval))
             end
 	  | _ -> 
- 	    pretype (mk_tycon tval) env evdref lvar c
+ 	    pretype (mk_tycon tval) env evdref lvar c, tval
 	in
 	let v = mkCast (cj.uj_val, k, tval) in
 	  { uj_val = v; uj_type = tval }
-- 
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 ++++-
 4 files changed, 22 insertions(+), 4 deletions(-)

(limited to 'pretyping')

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 *)
 
-- 
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 ++++--
 3 files changed, 11 insertions(+), 9 deletions(-)

(limited to 'pretyping')

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 *)
 
-- 
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 ++++++++
 4 files changed, 44 insertions(+), 30 deletions(-)

(limited to 'pretyping')

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*)
-- 
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(-)

(limited to 'pretyping')

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


From cb2b5cc48d54ada8a2899d311253fcb12a81fd14 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 8 Jul 2016 18:06:30 +0200
Subject: Remove spurious warnings about projections when requiring modules.

---
 pretyping/recordops.ml | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 682a883338..284af0cb15 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -195,7 +195,7 @@ let warn_projection_no_head_constant =
           ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
 
 (* Intended to always succeed *)
-let compute_canonical_projections (con,ind) =
+let compute_canonical_projections warn (con,ind) =
   let env = Global.env () in
   let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in
   let u = Univ.UContext.instance ctx in
@@ -222,7 +222,7 @@ let compute_canonical_projections (con,ind) =
 		 with Not_found ->
                      let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con)
                       and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
-                     warn_projection_no_head_constant (t,con_pp,proji_sp_pp);
+                     if warn then warn_projection_no_head_constant (t,con_pp,proji_sp_pp);
                    l
 	       end
 	   | _ -> l)
@@ -246,9 +246,8 @@ let warn_redundant_canonical_projection =
           ++ strbrk " by " ++ prj ++ strbrk " in "
           ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)
 
-let open_canonical_structure i (_,o) =
-  if Int.equal i 1 then
-    let lo = compute_canonical_projections o in
+let add_canonical_structure warn o =
+    let lo = compute_canonical_projections warn o in
     List.iter (fun ((proj,(cs_pat,_ as pat)),s) ->
       let l = try Refmap.find proj !object_table with Not_found -> [] in
       let ocs = try Some (assoc_pat cs_pat l)
@@ -260,11 +259,14 @@ let open_canonical_structure i (_,o) =
               and new_can_s = (Termops.print_constr s.o_DEF) in
               let prj = (Nametab.pr_global_env Id.Set.empty proj)
               and hd_val = (pr_cs_pattern cs_pat) in
-              warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s))
+              if warn then warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s))
           lo
 
-let cache_canonical_structure o =
-  open_canonical_structure 1 o
+let open_canonical_structure i (_, o) =
+  if Int.equal i 1 then add_canonical_structure false o
+
+let cache_canonical_structure (_, o) =
+  add_canonical_structure true o
 
 let subst_canonical_structure (subst,(cst,ind as obj)) =
   (* invariant: cst is an evaluable reference. Thus we can take *)
-- 
cgit v1.2.3