From 1011266b84371b34536dd5aa5afb3a44b8f8d53c Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 17 Nov 2011 10:34:57 +0000
Subject: 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
---
 plugins/firstorder/sequent.ml        | 2 +-
 plugins/subtac/subtac_classes.ml     | 3 +--
 plugins/subtac/subtac_pretyping_F.ml | 8 ++++++--
 3 files changed, 8 insertions(+), 5 deletions(-)

(limited to 'plugins')

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;
-- 
cgit v1.2.3