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

3 files changed, 55 insertions, 31 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index c95486df61..4ba26dcebc 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -307,8 +307,13 @@ let gl_make_case_nodep ind gl =
 let elimination_then_using tac predicate bindings c gl =
   let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
   let indclause  = mk_clenv_from gl (c,t) in
-  general_elim_then_using gl_make_elim
-    true None tac predicate bindings ind indclause gl
+  let isrec,mkelim =
+    if (Global.lookup_mind (fst ind)).mind_record
+    then false,gl_make_case_dep
+    else true,gl_make_elim
+  in
+  general_elim_then_using mkelim isrec
+    None tac predicate bindings ind indclause gl
 
 let case_then_using =
   general_elim_then_using gl_make_case_dep false
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index bf93530762..2f386def1f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -782,16 +782,48 @@ let general_elim_clause elimtac (c,lbindc) elim gl =
 let general_elim with_evars c e =
   general_elim_clause (elimination_clause_scheme with_evars) c e
 
+(* Case analysis tactics *)
+
+let general_case_analysis_in_context with_evars (c,lbindc) gl =
+  let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+  let sort = elimination_sort_of_goal gl in
+  let elim =
+    if occur_term c (pf_concl gl) then
+      pf_apply build_case_analysis_scheme gl mind true sort
+    else
+      pf_apply build_case_analysis_scheme_default gl mind sort in
+  general_elim with_evars (c,lbindc)
+    {elimindex = None; elimbody = (elim,NoBindings)} gl
+
+let general_case_analysis with_evars (c,lbindc as cx) =
+  match kind_of_term c with
+    | Var id when lbindc = NoBindings ->
+	tclTHEN (try_intros_until_id_check id)
+	  (general_case_analysis_in_context with_evars cx)
+    | _ ->
+	general_case_analysis_in_context with_evars cx
+
+let simplest_case c = general_case_analysis false (c,NoBindings)
+
 (* Elimination tactic with bindings but using the default elimination
  * constant associated with the type. *)
 
+exception IsRecord
+
+let is_record mind = (Global.lookup_mind (fst mind)).mind_record
+
 let find_eliminator c gl =
   let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+  if is_record ind then raise IsRecord;
   let c = lookup_eliminator ind (elimination_sort_of_goal gl) in
   {elimindex = None; elimbody = (c,NoBindings)}
 
 let default_elim with_evars (c,_ as cx) gl =
-  general_elim with_evars cx (find_eliminator c gl) gl
+  try general_elim with_evars cx (find_eliminator c gl) gl
+  with IsRecord ->
+    (* For records, induction principles aren't there by default anymore.
+       Instead, we do a case analysis instead. *)
+    general_case_analysis with_evars cx gl
 
 let elim_in_context with_evars c = function
   | Some elim ->
@@ -848,29 +880,6 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags) id i elimclause
 let general_elim_in with_evars id =
   general_elim_clause (elimination_in_clause_scheme with_evars id)
 
-(* Case analysis tactics *)
-
-let general_case_analysis_in_context with_evars (c,lbindc) gl =
-  let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-  let sort = elimination_sort_of_goal gl in
-  let elim =
-    if occur_term c (pf_concl gl) then
-      pf_apply build_case_analysis_scheme gl mind true sort
-    else
-      pf_apply build_case_analysis_scheme_default gl mind sort in
-  general_elim with_evars (c,lbindc)
-    {elimindex = None; elimbody = (elim,NoBindings)} gl
-
-let general_case_analysis with_evars (c,lbindc as cx) =
-  match kind_of_term c with
-    | Var id when lbindc = NoBindings ->
-	tclTHEN (try_intros_until_id_check id)
-	  (general_case_analysis_in_context with_evars cx)
-    | _ ->
-	general_case_analysis_in_context with_evars cx
-
-let simplest_case c = general_case_analysis false (c,NoBindings)
-
 (* Apply a tactic below the products of the conclusion of a lemma *)
 
 type conjunction_status =
@@ -2803,7 +2812,7 @@ let guess_elim isrec hyp0 gl =
   let mind,_ = pf_reduce_to_quantified_ind gl tmptyp0 in
   let s = elimination_sort_of_goal gl in
   let elimc =
-    if isrec then lookup_eliminator mind s
+    if isrec && not (is_record mind) then lookup_eliminator mind s
     else
       if use_dependent_propositions_elimination () &&
 	dependent_no_evar (mkVar hyp0) (pf_concl gl)
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 8804c60c82..6537ff10d7 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;