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/inductiveops.mli | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'pretyping/inductiveops.mli')

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/inductiveops.mli | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'pretyping/inductiveops.mli')

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/inductiveops.mli | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'pretyping/inductiveops.mli')

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