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

1 files changed, 11 insertions, 0 deletions

diff --git a/library/declare.ml b/library/declare.ml
index aa10cf314..7364031d5 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 =