diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/indschemes.ml | 18 |
1 files changed, 14 insertions, 4 deletions
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; |