Change Hint Resolve, Immediate to take a global reference as argument

instead of a general constr: this is the most common case and does
not loose generality (one can simply define constrs before Hint Resolving
them). Benefits:
- Natural semantics for typeclasses, not class resolution needed at
Hint Resolve time, meaning less trouble for users as well.
- Ability to [Hint Remove] any hint so declared.
- Simplifies the implementation as well.


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

3 files changed, 15 insertions, 1 deletions

diff --git a/library/declare.ml b/library/declare.ml
index aa10cf3143..7364031d52 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -180,6 +180,17 @@ let declare_constant ?(internal = UserVerbose) id (cd,kind) =
   !xml_declare_constant (internal,kn);
   kn
 
+let declare_definition ?(internal=UserVerbose) ?(opaque=false) ?(kind=Decl_kinds.Definition)
+  id ?types body =
+  let cb = 
+    { Entries.const_entry_body = body;
+      const_entry_type = types;
+      const_entry_opaque = opaque;
+      const_entry_secctx = None }
+  in
+    declare_constant ~internal id
+      (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) 
+
 (** Declaration of inductive blocks *)
 
 let declare_inductive_argument_scopes kn mie =
diff --git a/library/declare.mli b/library/declare.mli
index 6f69f673ee..9cc6e371ca 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -57,6 +57,10 @@ type internal_flag =
 val declare_constant :
  ?internal:internal_flag -> identifier -> constant_declaration -> constant
 
+val declare_definition : 
+  ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
+  identifier -> ?types:constr -> constr -> constant
+
 (** [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
    the whole block (boolean must be true iff it is a record) *)
diff --git a/library/global.mli b/library/global.mli
index ff3c731998..82b7cc8eb0 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -101,6 +101,5 @@ val import : compiled_library -> Digest.t -> module_path
 val type_of_global : Globnames.global_reference -> types
 val env_of_context : Environ.named_context_val -> Environ.env
 
-
 (** spiwack: register/unregister function for retroknowledge *)
 val register : Retroknowledge.field -> constr -> constr -> unit