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.
---
 tactics/elimschemes.ml  | 4 ++++
 tactics/elimschemes.mli | 2 ++
 2 files changed, 6 insertions(+)

(limited to 'tactics')

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
 
 
-- 
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

---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

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:
-- 
cgit v1.2.3