* removed declare_constant and declare_internal_constant

(declare_constant_gen was not exported, leading to a lot of silly tests
before calling those functions) and replaced them by
declare_constant : ?internal:internal_flat -> ...

declare_constant's default behaviour is the same as the old declare_constant.

* fixed the default behaviour of inductive scheme failure during coq's
 compilation.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13395 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 18 insertions, 28 deletions

diff --git a/library/declare.ml b/library/declare.ml
index b0af8d5180..0764af4b06 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -172,17 +172,12 @@ let declare_constant_common id dhyps (cd,kind) =
   Notation.declare_ref_arguments_scope (ConstRef c);
   c
 
-let declare_constant_gen internal id (cd,kind) =
+let declare_constant ?(internal = UserVerbose) id (cd,kind) =
   let cd = hcons_constant_declaration cd in
   let kn = declare_constant_common id [] (ConstantEntry cd,kind) in
   !xml_declare_constant (internal,kn);
   kn
 
-(* TODO: add a third function to distinguish between KernelVerbose
- * and user Verbose *)
-let declare_internal_constant = declare_constant_gen KernelSilent
-let declare_constant = declare_constant_gen UserVerbose
-
 (** Declaration of inductive blocks *)
 
 let declare_inductive_argument_scopes kn mie =
diff --git a/library/declare.mli b/library/declare.mli
index b6ed0a815d..1ad733816f 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -43,17 +43,19 @@ type constant_declaration = constant_entry * logical_kind
 
 (** [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
-   the full path of the declaration *)
+   the full path of the declaration 
+
+  internal specify if the constant has been created by the kernel or by the
+  user, and in the former case, if its errors should be silent
+   
+   *)
 type internal_flag =
   | KernelVerbose
   | KernelSilent
   | UserVerbose
 
 val declare_constant :
- identifier -> constant_declaration -> constant
-
-val declare_internal_constant :
-  identifier -> constant_declaration -> constant
+ ?internal:internal_flag -> identifier -> constant_declaration -> constant
 
 (** [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index c792367c3b..0e9281a21d 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1464,7 +1464,7 @@ let add_morphism_infer glob m n =
   let instance_id = add_suffix n "_Proper" in
   let instance = build_morphism_signature m in
     if Lib.is_modtype () then
-      let cst = Declare.declare_internal_constant instance_id
+      let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id
 				(Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
 	add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst));
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2069cc23f3..b253b2375e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3473,7 +3473,7 @@ let abstract_subproof id tac gl =
   let const = Pfedit.build_constant_by_tactic secsign concl
     (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in
   let cd = Entries.DefinitionEntry const in
-  let lem = mkConst (Declare.declare_internal_constant id (cd,IsProof Lemma)) in
+  let lem = mkConst (Declare.declare_constant ~internal:Declare.KernelSilent id (cd,IsProof Lemma)) in
   exact_no_check
     (applist (lem,List.rev (Array.to_list (instance_from_named_context sign))))
     gl
@@ -3503,7 +3503,7 @@ let admit_as_an_axiom gl =
   if occur_existential concl then error"\"admit\" cannot handle existentials.";
   let axiom =
     let cd = Entries.ParameterEntry (concl,false) in
-    let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in
+    let con = Declare.declare_constant ~internal:Declare.KernelSilent na (cd,IsAssumption Logical) in
     constr_of_global (ConstRef con)
   in
   exact_no_check
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index ea3a888ecc..c06fbfc685 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -187,7 +187,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 	    Evarutil.nf_evar !evars t
 	in
 	Evarutil.check_evars env Evd.empty !evars termtype;
-	let cst = Declare.declare_internal_constant id
+	let cst = Declare.declare_constant ~internal:Declare.KernelSilent id
 	  (Entries.ParameterEntry (termtype,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
 	in instance_hook k None false imps ?hook (ConstRef cst); id
       end
@@ -301,7 +301,7 @@ let context ?(hook=fun _ -> ()) l =
   in
   let fn (id, _, t) =
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
-      let cst = Declare.declare_internal_constant id
+      let cst = Declare.declare_constant ~internal:Declare.KernelSilent id
 	(ParameterEntry (t,false), IsAssumption Logical)
       in
 	match class_of_constr t with
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 974b74a6df..3440f9fe85 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -110,11 +110,7 @@ let declare_scheme kind indcl =
   Lib.add_anonymous_leaf (inScheme (kind,indcl))
 
 let define internal id c =
-  (* TODO: specify even more by distinguish between KernelVerbose and
-   * UserVerbose *)
-  let fd = match internal with 
-    | KernelSilent -> declare_internal_constant
-    | _ -> declare_constant in
+  let fd = declare_constant ~internal in
   let kn = fd id
     (DefinitionEntry
       { const_entry_body = c;
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 3b090e79e1..8d8997a2b4 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -79,7 +79,7 @@ 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;
@@ -100,10 +100,7 @@ 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;
@@ -121,8 +118,8 @@ let declare_beq_scheme_gen internal names kn =
 
 let alarm what internal msg =
   let debug = false in
-  (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *)
   match internal with
+  | KernelVerbose 
   | KernelSilent ->
     (if debug then
       Flags.if_verbose Pp.msg_warning
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 0b338fdd8a..0dd18f0641 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -193,7 +193,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
                     const_entry_opaque = false;
 		    const_entry_boxed = Flags.boxed_definitions() } in
 		  let k = (DefinitionEntry cie,IsDefinition kind) in
-		  let kn = declare_internal_constant fid k in
+		  let kn = declare_constant ~internal:KernelSilent fid k in
 		  Flags.if_verbose message (string_of_id fid ^" is defined");
 		  kn
                 with Type_errors.TypeError (ctx,te) ->