From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 toplevel/indschemes.ml | 27 ++++++++++++++-------------
 1 file changed, 14 insertions(+), 13 deletions(-)

(limited to 'toplevel/indschemes.ml')

diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 3596085f..51eddbae 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indschemes.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (* Created by Hugo Herbelin from contents related to inductive schemes
    initially developed by Christine Paulin (induction schemes), Vincent
    Siles (decidable equality and boolean equality) and Matthieu Sozeau
@@ -49,6 +47,7 @@ let elim_flag = ref true
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "automatic declaration of induction schemes";
       optkey   = ["Elimination";"Schemes"];
       optread  = (fun () -> !elim_flag) ;
@@ -58,6 +57,7 @@ let case_flag = ref false
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "automatic declaration of case analysis schemes";
       optkey   = ["Case";"Analysis";"Schemes"];
       optread  = (fun () -> !case_flag) ;
@@ -67,6 +67,7 @@ let eq_flag = ref false
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "automatic declaration of boolean equality";
       optkey   = ["Boolean";"Equality";"Schemes"];
       optread  = (fun () -> !eq_flag) ;
@@ -74,6 +75,7 @@ let _ =
 let _ = (* compatibility *)
   declare_bool_option
     { optsync  = true;
+      optdepr  = true;
       optname  = "automatic declaration of boolean equality";
       optkey   = ["Equality";"Scheme"];
       optread  = (fun () -> !eq_flag) ;
@@ -81,10 +83,11 @@ let _ = (* compatibility *)
 
 let is_eq_flag () = !eq_flag && Flags.version_strictly_greater Flags.V8_2
 
-let eq_dec_flag = ref false
+let eq_dec_flag = ref false 
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "automatic declaration of decidable equality";
       optkey   = ["Decidable";"Equality";"Schemes"];
       optread  = (fun () -> !eq_dec_flag) ;
@@ -94,6 +97,7 @@ let rewriting_flag = ref false
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  ="automatic declaration of rewriting schemes for equality types";
       optkey   = ["Rewriting";"Schemes"];
       optread  = (fun () -> !rewriting_flag) ;
@@ -102,16 +106,13 @@ let _ =
 (* Util *)
 
 let define id internal c t =
-  (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *)
-  let f = match internal with
-   | KernelSilent -> declare_internal_constant
-   | _ -> declare_constant in
+  let f = declare_constant ~internal in
   let kn = f id
     (DefinitionEntry
       { const_entry_body = c;
+        const_entry_secctx = None;
         const_entry_type = t;
-        const_entry_opaque = false;
-	const_entry_boxed = Flags.boxed_definitions() },
+        const_entry_opaque = false },
       Decl_kinds.IsDefinition Scheme) in
   definition_message id;
   kn
@@ -127,7 +128,7 @@ let alarm what internal msg =
   | KernelVerbose 
   | KernelSilent ->
     (if debug then
-      Flags.if_verbose Pp.msg_warning
+      Flags.if_warn Pp.msg_warning
 	(hov 0 msg ++ fnl () ++ what ++ str " not defined."))
   | _ -> errorlabstrm "" msg
 
@@ -158,7 +159,7 @@ let try_declare_scheme what f internal names kn =
 	  (strbrk "Required constant " ++ str s ++ str " undefined.")
     | AlreadyDeclared msg ->
         alarm what internal (msg ++ str ".")
-    | _ ->
+    | _ -> 
 	alarm what internal
 	  (str "Unknown exception during scheme creation.")
 
@@ -173,7 +174,7 @@ let declare_beq_scheme_with l kn =
   try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn
 
 let try_declare_beq_scheme kn =
-  (* TODO: handle Fix, see e.g. TheoryList.In_spec, eventually handle
+  (* TODO: handle Fix, eventually handle
       proof-irrelevance; improve decidability by depending on decidability
       for the parameters rather than on the bl and lb properties *)
   try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelVerbose [] kn
-- 
cgit v1.2.3