From 58c5203fce255255b919ed04fd94eece9afb90a0 Mon Sep 17 00:00:00 2001
From: vsiles
Date: Tue, 17 Apr 2007 16:16:55 +0000
Subject:  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
---
 CHANGES             |  3 +++
 toplevel/command.ml | 14 +++++++++++++-
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index b176fb6856..aa8a594135 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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 =
-- 
cgit v1.2.3