Merge PR#613: Cumulativity for inductive types

3 files changed, 27 insertions, 18 deletions

diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 466b1350d..99761437e 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -47,7 +47,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
       (nf c', Evd.evar_universe_context sigma), eff
   else
     let mib,mip = Inductive.lookup_mind_specif env ind in
-    let ctx = Declareops.inductive_context mib in
+    let ctx = Declareops.inductive_polymorphic_context mib in
     let u = Univ.UContext.instance ctx in
     let ctxset = Univ.ContextSet.of_context ctx in
     let ectx = Evd.evar_universe_context_of ctxset in
@@ -60,7 +60,7 @@ let build_induction_scheme_in_type dep sort ind =
   let sigma = Evd.from_env env in
   let ctx = 
     let mib,mip = Inductive.lookup_mind_specif env ind in
-      Declareops.inductive_context mib
+      Declareops.inductive_polymorphic_context mib
   in
   let u = Univ.UContext.instance ctx in
   let ctxset = Univ.ContextSet.of_context ctx in
@@ -80,30 +80,30 @@ let rect_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
     (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants)
 
-let ind_scheme_kind_from_type =
-  declare_individual_scheme_object "_ind_nodep"
-  (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InProp)
-
-let ind_scheme_kind_from_prop =
-  declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
-  (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InProp)
-
-let ind_dep_scheme_kind_from_type =
-  declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
-  (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InProp)
+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_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)
 
+let ind_scheme_kind_from_type =
+  declare_individual_scheme_object "_ind_nodep"
+  (optimize_non_type_induction_scheme rec_scheme_kind_from_type false InProp)
+
+let ind_dep_scheme_kind_from_type =
+  declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
+  (optimize_non_type_induction_scheme rec_dep_scheme_kind_from_type true InProp)
+
+let ind_scheme_kind_from_prop =
+  declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
+  (optimize_non_type_induction_scheme rec_scheme_kind_from_prop false InProp)
+
 (* Case analysis *)
 
 let build_case_analysis_scheme_in_type dep sort ind =
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index 77f927f2d..da432bead 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -10,6 +10,14 @@ open Ind_tables
 
 (** Induction/recursion schemes *)
 
+val optimize_non_type_induction_scheme : 
+  'a Ind_tables.scheme_kind ->
+  Indrec.dep_flag ->
+  Term.sorts_family ->
+  'b ->
+  Names.inductive ->
+  (Constr.constr * Evd.evar_universe_context) * Safe_typing.private_constants
+
 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
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 681db5d08..2fc8baa89 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1306,7 +1306,8 @@ let interp_hints poly =
           List.init (nconstructors ind) 
 	    (fun i -> let c = (ind,i+1) in
 		      let gr = ConstructRef c in
-			empty_hint_info, mib.Declarations.mind_polymorphic, true,
+			empty_hint_info, 
+                        (Declareops.inductive_is_polymorphic mib), true,
 			PathHints [gr], IsGlobRef gr)
       in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
   | HintsExtern (pri, patcom, tacexp) ->