Merge subinstances branch by me and Tom Prince.

This adds two experimental features to the typeclass implementation:
- Path cuts: a way to specify through regular expressions on instance names
search pathes that should be avoided (e.g. [proper_flip proper_flip]).
Regular expression matching is implemented through naïve derivatives.
- Forward hints for subclasses: e.g. [Equivalence -> Reflexive] is no
longer applied backwards, but introducing a specific [Equivalence] in the
environment register a [Reflexive] hint as well. Currently not
backwards-compatible, the next patch will allow to specify direction
of subclasses hints.

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

3 files changed, 8 insertions, 5 deletions

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 571ec4ef34..f75678c60f 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -210,7 +210,7 @@ open Auto
 
 let extend_with_auto_hints l seq gl=
   let seqref=ref seq in
-  let f (_, p_a_t) =
+  let f p_a_t =
     match p_a_t.code with
 	Res_pf (c,_) | Give_exact c
       | Res_pf_THEN_trivial_fail (c,_) ->
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 000ffc6226..c08dd16df5 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -179,9 +179,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
   Evarutil.check_evars env Evd.empty !evars termtype;
   let hook vis gr =
     let cst = match gr with ConstRef kn -> kn | _ -> assert false in
-    let inst = Typeclasses.new_instance k pri global (ConstRef cst) in
       Impargs.declare_manual_implicits false gr ~enriching:false [imps];
-      Typeclasses.add_instance inst
+      Typeclasses.declare_instance pri (not global) (ConstRef cst)
   in
   let evm = Subtac_utils.evars_of_term !evars Evd.empty term in
   let obls, _, constr, typ = Eterm.eterm_obligations env id !evars evm 0 term termtype in
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index d300a71ccc..d5d427c7a6 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -599,8 +599,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  (pretype_type empty_valcon env evdref lvar c).utj_val 
     in
       if resolve_classes then
-	evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
-	  ~split:true ~fail:fail_evar env !evdref;
+	(try 
+	   evdref := Typeclasses.resolve_typeclasses ~onlyargs:true
+	     ~split:true ~fail:true env !evdref;
+	   evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
+	     ~split:true ~fail:false env !evdref
+	 with e -> if fail_evar then raise e else ());
       evdref := consider_remaining_unif_problems env !evdref;
       let c = if expand_evar then nf_evar !evdref c' else c' in
       if fail_evar then check_evars env Evd.empty !evdref c;