From 0919391f43729bf172ab00c8dec9438a0a9f59ab Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 26 Oct 2012 01:29:33 +0000 Subject: 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 --- library/global.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'library/global.mli') diff --git a/library/global.mli b/library/global.mli index ff3c73199..82b7cc8eb 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 -- cgit v1.2.3