Syntax changes in typeclasses, remove "?" for usual implicit arguments

binding, add "!" syntax for the new binders which require parameters and
not superclasses. Change backquotes for curly braces for user-given
implicit arguments, following tradition. This requires a hack a la
lpar-id-coloneq. Change ident to global for typeclass names in class
binders. Also requires a similar hack to distinguish between [ C t1 tn ]
and [ c : C t1 tn ]. Update affected theories.

While hacking the parsing of { wf }, factorized the two versions of fix
annotation parsing that were present in g_constr and g_vernac.

Add the possibility of the user optionaly giving the priority for resolve and
exact hints (used by type classes). Syntax not fixed yet: a natural
after the list of lemmas in "Hint Resolve" syntax, a natural after a "|"
after the instance constraint in Instance declarations (ex in
Morphisms.v).


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

1 files changed, 13 insertions, 2 deletions

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index f231c7406d..c06006ad05 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -10,6 +10,7 @@
 
 (*i*)
 open Names
+open Libnames
 open Decl_kinds
 open Term
 open Sign
@@ -41,8 +42,8 @@ type typeclass = {
 
 type instance = {
   is_class: typeclass;
-  is_name: identifier; (* Name of the instance *)
-  is_impl: constant; 
+  is_pri : int option;
+  is_impl: constant;
 }
   
 val instances : Libnames.reference -> instance list
@@ -50,6 +51,9 @@ val typeclasses : unit -> typeclass list
 val add_class : typeclass -> unit
 val add_instance : instance -> unit
 
+val register_add_instance_hint : (reference -> int option -> unit) -> unit
+val add_instance_hint : reference -> int option -> unit
+
 val class_info : identifier -> typeclass (* raises Not_found *)
 val class_of_inductive : inductive -> typeclass (* raises Not_found *)
 
@@ -75,3 +79,10 @@ val substitution_of_named_context :
 val nf_substitution : evar_map -> substitution -> substitution
 
 val is_implicit_arg : hole_kind -> bool
+
+
+val subst :  'a * Mod_subst.substitution *
+    ((Names.identifier, typeclass) Gmap.t * 'b * ('c, instance list) Gmap.t) ->
+    (Names.identifier, typeclass) Gmap.t * 'b * ('c, instance list) Gmap.t
+
+val qualid_of_con : Names.constant -> Libnames.reference