Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant

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

1 files changed, 6 insertions, 9 deletions

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 36c2bbb23a..853bc7ccd9 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -35,21 +35,18 @@ val push_named_def :
 val pop_named_decls : identifier list -> safe_environment -> safe_environment
 
 (* Adding global axioms or definitions *)
-
-val add_parameter :
-  section_path -> constr -> safe_environment -> safe_environment
-
-(*s Global and local constant declaration. *)
-
 type constant_entry = {
   const_entry_body   : constr;
   const_entry_type   : types option;
   const_entry_opaque : bool }
 
+type global_declaration = 
+  | ConstantEntry of constant_entry
+  | ParameterEntry of types
+  | GlobalRecipe of Cooking.recipe
+
 val add_constant : 
-  section_path -> constant_entry -> safe_environment -> safe_environment
-val add_discharged_constant : 
-  section_path -> Cooking.recipe -> safe_environment -> safe_environment
+  section_path -> global_declaration -> safe_environment -> safe_environment
 
 (* Adding an inductive type *)
 val add_mind :