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

6 files changed, 27 insertions, 11 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 82fbe9c691..7cc43e4ce8 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -467,6 +467,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	   try 
 	     [make_apply_entry (pf_env g') (project g')
 		(true,false) 
+		None
 		(mkVar hid,htyp)]
 	   with Failure _ -> [] 
 	 in
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index db8963554b..4d28a22a98 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1727,7 +1727,7 @@ let rec xlate_vernac =
 		      CT_id_ne_list(n1, names), dblist)
 	| HintsExtern (n, c, t) ->
 	    CT_hint_extern(CT_int n, xlate_formula c, xlate_tactic t, dblist)
-        | HintsResolve l | HintsImmediate l -> 
+        | HintsImmediate l -> 
 	 let f1, formulas = match List.map xlate_formula l with
 	     a :: tl -> a, tl
 	   | _  -> failwith "" in
@@ -1744,6 +1744,23 @@ let rec xlate_vernac =
 		  HintsResolve _ -> CT_hints_resolve(l', dblist)
 		| HintsImmediate _ -> CT_hints_immediate(l', dblist)
 		| _ -> assert false)
+        | HintsResolve l -> 
+	 let f1, formulas = match List.map xlate_formula (List.map snd l) with
+	     a :: tl -> a, tl
+	   | _  -> failwith "" in
+	 let l' = CT_formula_ne_list(f1, formulas) in
+	   if local then
+             (match h with 
+		  HintsResolve _ ->
+		    CT_local_hints_resolve(l', dblist)
+	       	| HintsImmediate _ ->
+		    CT_local_hints_immediate(l', dblist)
+	       	| _ -> assert false)
+	   else
+	     (match h with
+		  HintsResolve _ -> CT_hints_resolve(l', dblist)
+		| HintsImmediate _ -> CT_hints_immediate(l', dblist)
+		| _ -> assert false)
         | HintsUnfold l -> 
 	 let n1, names = match List.map loc_qualid_to_ct_ID l with
 	     n1 :: names -> n1, names
@@ -2083,7 +2100,7 @@ let rec xlate_vernac =
 
     (* TypeClasses *) 
    | VernacDeclareInstance _|VernacContext _|
-	 VernacInstance (_, _, _)|VernacClass (_, _, _, _, _) ->
+	 VernacInstance (_, _, _, _)|VernacClass (_, _, _, _, _) ->
 	   xlate_error "TODO: Type Classes commands"
 
   | VernacResetName id -> CT_reset (xlate_ident (snd id))
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index e9c2ed4e52..2d1be640b1 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -148,8 +148,8 @@ let subtac (loc, command) =
       | VernacAssumption (stre,nl,l) -> 
 	  vernac_assumption env isevars stre l nl
 
-      | VernacInstance (sup, is, props) ->
-	  ignore(Subtac_classes.new_instance sup is props)
+      | VernacInstance (sup, is, props, pri) ->
+	  ignore(Subtac_classes.new_instance sup is props pri)
 
       | VernacCoFixpoint (l, b) ->
 	  let _ = trace (str "Building cofixpoint") in
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index e439021635..a2184a557e 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -100,7 +100,7 @@ let type_class_instance_params isevars env id n ctx inst subst =
 let substitution_of_constrs ctx cstrs =
   List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx []
 
-let new_instance ctx (instid, bk, cl) props =
+let new_instance ctx (instid, bk, cl) props pri =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
   let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in
@@ -211,11 +211,10 @@ let new_instance ctx (instid, bk, cl) props =
   let hook cst = 
     let inst = 
       { is_class = k;
-	is_name = id;
+	is_pri = pri;
 	is_impl = cst;
       }
     in
-      Classes.add_instance_hint id;
       Impargs.declare_manual_implicits false (ConstRef cst) false imps;
       Typeclasses.add_instance inst
   in
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
index 12a6e29549..c621f1516f 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/contrib/subtac/subtac_classes.mli
@@ -36,4 +36,5 @@ val new_instance :
   Topconstr.local_binder list ->
   typeclass_constraint ->
   binder_def_list ->
+  int option ->
   identifier
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 5bcbf4db6c..730b12605e 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -572,11 +572,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
       | IsType ->
 	  (pretype_type empty_valcon env isevars lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !isevars in
-    let evd = nf_evar_defs evd in
     let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (evars_of evd) evd in
-    let c' = nf_evar (evars_of evd) c' in
-      isevars := evd;
-      c'
+      isevars:=evd;
+      nf_evar (evars_of !isevars) c'
 
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage