From 06e6a7b5a0d15f493a3f94fad905af2c44be9c09 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 3 Sep 2014 16:47:54 +0200
Subject: Type definitions with [Variant] don't generate inductive schemes by
 default.

- The option [Record Elimination Schemes] is replaced by [Nonrecursive Elimination Schemes] ([Record Elimination Schemes] is kept as a deprecated option for compatibility)
- [Variant] don't generate inductive scheme unless [Nonrecursive Elimination Schemes] is turned on.
- Inductive records generate induction schemes even when [Nonrecursive Elimination Schemes] is off.
---
 toplevel/indschemes.ml | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 7db71c0979..1ecd893d92 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -51,15 +51,23 @@ let _ =
       optread  = (fun () -> !elim_flag) ;
       optwrite = (fun b -> elim_flag := b) }
 
-let record_elim_flag = ref false
+let bifinite_elim_flag = ref false
 let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
-      optname  = "automatic declaration of induction schemes for records";
+      optname  = "automatic declaration of induction schemes for non-recursive types";
+      optkey   = ["Nonrecursive";"Elimination";"Schemes"];
+      optread  = (fun () -> !bifinite_elim_flag) ;
+      optwrite = (fun b -> bifinite_elim_flag := b) }
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = true; (* compatibility 2014-09-03*)
+      optname  = "automatic declaration of induction schemes for non-recursive types";
       optkey   = ["Record";"Elimination";"Schemes"];
-      optread  = (fun () -> !record_elim_flag) ;
-      optwrite = (fun b -> record_elim_flag := b) }
+      optread  = (fun () -> !bifinite_elim_flag) ;
+      optwrite = (fun b -> bifinite_elim_flag := b) }
 
 let case_flag = ref false
 let _ =
@@ -469,7 +477,7 @@ 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_record = None || !record_elim_flag) then
+  if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) 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