diff options
| author | vsiles | 2007-04-17 16:16:55 +0000 |
|---|---|---|
| committer | vsiles | 2007-04-17 16:16:55 +0000 |
| commit | 58c5203fce255255b919ed04fd94eece9afb90a0 (patch) | |
| tree | 64ac3dcf8a8a6a0cc2f19e9c4074e0f7807c48b8 | |
| parent | f5778254f73e483d755402a5b85c7843770191ca (diff) | |
Added the option to set/unset the automatic generation of elimination schemes
Set Elimination Schemes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9780 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | toplevel/command.ml | 14 |
2 files changed, 16 insertions, 1 deletions
@@ -6,6 +6,9 @@ Commands - Added option Global to "Implicit Arguments" and "Arguments Scope" for section surviving. +- Added option "Unset Elimination Schemes" to deactivated the automatic +generation of elimination schemes. + Notations - Level "constr" moved from 9 to 8. diff --git a/toplevel/command.ml b/toplevel/command.ml index ecd0a6d7e3..12146cdee4 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -413,11 +413,23 @@ let prepare_inductive ntnl indl = }) indl in List.fold_right option_cons ntnl [], indl +open Goptions + +let elim_flag = ref true +let _ = + declare_bool_option + { optsync = true; + optname = "automatic declaration of eliminations"; + optkey = (SecondaryTable ("Elimination","Schemes")); + optread = (fun () -> !elim_flag) ; + optwrite = (fun b -> elim_flag := b) } + + let declare_mutual_with_eliminations isrecord mie = let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in let (_,kn) = declare_mind isrecord mie in if_verbose ppnl (minductive_message names); - declare_eliminations kn; + if !elim_flag then declare_eliminations kn; kn let build_mutual l finite = |