Let's try to avoid generating induction principles for records (wish #2693)

 Since record cannot be recursive, induction principles for them are
 just wasted ressources. With this patch, we turn off there generation
 by default. The flag "Set/Unset Record Elimination Schemes" allows
 to start producing them again.

 For compatibility, we adapt "induction" and similar tactics that
 rely on the existence of induction principles : on a record,
 "induction" is now silently converted into "destruct".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15411 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 4 deletions

diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 8804c60c8..6537ff10d 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -55,6 +55,16 @@ let _ =
       optread  = (fun () -> !elim_flag) ;
       optwrite = (fun b -> elim_flag := b) }
 
+let record_elim_flag = ref false
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "automatic declaration of induction schemes for records";
+      optkey   = ["Record";"Elimination";"Schemes"];
+      optread  = (fun () -> !record_elim_flag) ;
+      optwrite = (fun b -> record_elim_flag := b) }
+
 let case_flag = ref false
 let _ =
   declare_bool_option
@@ -448,11 +458,11 @@ let do_combined_scheme name schemes =
 
 let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done
 
-let mutual_inductive_size kn = Array.length (Global.lookup_mind kn).mind_packets
-
 let declare_default_schemes kn =
-  let n = mutual_inductive_size kn in
-  if !elim_flag then declare_induction_schemes kn;
+  let mib = Global.lookup_mind kn in
+  let n = Array.length mib.mind_packets in
+  if !elim_flag && (not mib.mind_record || !record_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;
   if !eq_dec_flag then try_declare_eq_decidability kn;