Fix the clrewrite tactic, change Relations.v to work on relations in Prop

only, and get rid of the "relation" definition which makes unification
fail blatantly. Replace it with a notation :) In its current state,
the new tactic seems ready for larger tests.


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

8 files changed, 84 insertions, 100 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 3a834ff8a8..5dc06f33cc 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1192,8 +1192,6 @@ Check (fun l:list (list nat) => map length l).
 \Rem To know which are the implicit arguments of an object, use the command
 {\tt Print Implicit} (see \ref{PrintImplicit}).
 
-\Rem 
-
 \Rem If the list of arguments is empty, the command removes the
 implicit arguments of {\qualid}.
 
diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4
index 84c1937ea8..9aa4451870 100644
--- a/tactics/class_setoid.ml4
+++ b/tactics/class_setoid.ml4
@@ -74,7 +74,8 @@ let iff_equiv = lazy (gen_constant ["Classes"; "Relations"] "iff_equivalence")
 let eq_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_equivalence")
 
 (* let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") *)
-let coq_relation = lazy (gen_constant ["Classes";"Relations"] "relation")
+(* let coq_relation = lazy (gen_constant ["Classes";"Relations"] "relation") *)
+let coq_relation a = mkProd (Anonymous, a, mkProd (Anonymous, a, mkProp))
 let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT")
 
 let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv_refl")
@@ -112,7 +113,7 @@ let build_signature isevars env m cstrs finalcstr =
       (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t
   in
   let mk_relty ty obj =
-    let relty = mkApp (Lazy.force coq_relation, [| ty |]) in
+    let relty = coq_relation ty in
       match obj with
 	| None -> new_evar isevars env relty
 	| Some (p, (a, r, oldt, newt)) -> r
@@ -256,17 +257,13 @@ let decompose_setoid_eqhyp gl env sigma c left2right t =
 	  let relargs, args = array_chop (Array.length args - 2) args in
 	  let rel = mkApp (r, relargs) in
 	  let typ = pf_type_of gl rel in
-	    (match kind_of_term typ with
-	      | App (relation, [| carrier |]) when eq_constr relation (Lazy.force coq_relation) 
-		    || eq_constr relation (Lazy.force coq_relationT) ->
-		  (c, (carrier, rel, args.(0), args.(1)))
-	      | _ when isArity typ ->
-		  let (ctx, ar) = destArity typ in
-		    (match ctx with
-			[ (_, None, sx) ; (_, None, sy) ] when eq_constr sx sy -> 
-			  (c, (sx, rel, args.(0), args.(1)))
-		      | _ -> error "Only binary relations are supported")
-	      | _ -> error "Not a relation")
+	    (if isArity typ then
+	      let (ctx, ar) = destArity typ in
+		(match ctx with
+		    [ (_, None, sx) ; (_, None, sy) ] when eq_constr sx sy -> 
+		      (c, (sx, rel, args.(0), args.(1)))
+		  | _ -> error "Only binary relations are supported")
+	      else error "Not a relation")
       | _ -> error "Not a relation"
   in
     if left2right then res
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 70ec9d046e..da477f2a32 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -241,15 +241,19 @@ module SearchProblem = struct
 
   let success s = (sig_it (fst s.tacres)) = []
 
-  let rec filter_tactics (glls,v) = function
-    | [] -> []
-    | (tac,pptac) :: tacl -> 
-	try 
-	  let (lgls,ptl) = apply_tac_list tac glls in 
-	  let v' p = v (ptl p) in
-	  ((lgls,v'),pptac) :: filter_tactics (glls,v) tacl
-	with e when Logic.catchable_exception e ->
-	  filter_tactics (glls,v) tacl
+  let filter_tactics (glls,v) l =
+(*     let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
+    let rec aux = function
+      | [] -> []
+      | (tac,pptac) :: tacl -> 
+	  try 
+	    let (lgls,ptl) = apply_tac_list tac glls in 
+	    let v' p = v (ptl p) in
+(* 	      msg (hov 0 (pptac ++ str"\n")); *)
+	      ((lgls,v'),pptac) :: aux tacl
+	  with e when Logic.catchable_exception e ->
+	    aux tacl
+    in aux l
 
   (* Ordering of states is lexicographic on depth (greatest first) then
      number of remaining goals. *)
@@ -498,7 +502,7 @@ let valid evm p res_sigma l =
       !res_sigma (l, Evd.create_evar_defs !res_sigma)
   in raise (Found (snd evd'))
     
-let resolve_all_evars debug (mode, depth) env p evd =
+let resolve_all_evars_once debug (mode, depth) env p evd =
   let evm = Evd.evars_of evd in
   let goals = 
     Evd.fold
@@ -513,3 +517,16 @@ let resolve_all_evars debug (mode, depth) env p evd =
   let gls', valid' = full_eauto_gls debug (mode, depth) [] (gls, valid evm p res_sigma) in
     res_sigma := Evarutil.nf_evars (sig_sig gls');
     try ignore(valid' []); assert(false) with Found evd' -> Evarutil.nf_evar_defs evd'
+
+let has_undefined p evd =
+  Evd.fold (fun ev evi has -> has ||
+    (evi.evar_body = Evar_empty && p ev evi))
+    (Evd.evars_of evd) false
+    
+let rec resolve_all_evars debug m env p evd =
+  let rec aux n evd = 
+    if has_undefined p evd && n > 0 then
+      let evd' = resolve_all_evars_once debug m env p evd in
+	aux (pred n) evd'
+    else evd
+  in aux 3 evd
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 940648c2eb..a1ff899053 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -61,6 +61,9 @@ end
 val full_eauto_gls : bool -> bool * int -> constr list -> goal list sigma * validation -> 
   goal list sigma * validation
 
+val resolve_all_evars_once : bool -> bool * int -> env -> (evar -> evar_info -> bool) -> evar_defs ->
+  evar_defs
+
 val resolve_all_evars : bool -> bool * int -> env -> (evar -> evar_info -> bool) -> evar_defs ->
   evar_defs
 
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 09a58fa019..72db276e4a 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -29,23 +29,16 @@ Unset Strict Implicit.
 
 (** Respectful morphisms. *)
 
-Definition respectful_depT (A : Type) (R : relationT A) 
-  (B : A -> Type) (R' : forall x y, B x -> B y -> Type) : relationT (forall x : A, B x) := 
+Definition respectful_dep (A : Type) (R : relation A) 
+  (B : A -> Type) (R' : forall x y, B x -> B y -> Prop) : relation (forall x : A, B x) := 
   fun f g => forall x y : A, R x y -> R' x y (f x) (g y).
 
-Definition respectfulT A (eqa : relationT A) B (eqb : relationT B) : relationT (A -> B) :=
-  Eval compute in (respectful_depT eqa (fun _ _ => eqb)).
-
 Definition respectful A (R : relation A) B (R' : relation B) : relation (A -> B) :=
   fun f g => forall x y : A, R x y -> R' (f x) (g y).
 
-(** Notations reminiscent of the old syntax for declaring morphisms.
-   We use three + or - for type morphisms, and two for [Prop] ones.
-   *)
-
-Notation " R +++> R' " := (@respectfulT _ R _ R') (right associativity, at level 20).
-Notation " R ---> R' " := (@respectfulT _ (flip R) _ R') (right associativity, at level 20).
+(** Notations reminiscent of the old syntax for declaring morphisms. *)
 
+Notation " R ==> R' " := (@respectful _ R _ R') (right associativity, at level 20).
 Notation " R ++> R' " := (@respectful _ R _ R') (right associativity, at level 20).
 Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity, at level 20).
 
@@ -53,7 +46,7 @@ Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity,
    The relation [R] will be instantiated by [respectful] and [A] by an arrow type 
    for usual morphisms. *)
 
-Class Morphism A (R : relationT A) (m : A) :=
+Class Morphism A (R : relation A) (m : A) :=
   respect : R m m.
 
 (** Here we build an equivalence instance for functions which relates respectful ones only. *)
@@ -63,7 +56,7 @@ Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : rela
 
 Ltac obligations_tactic ::= program_simpl.
 
-Program Instance [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] => 
+Program Instance [ Equivalence A R, Equivalence B R' ] => 
   respecting_equiv : Equivalence respecting
   (fun (f g : respecting) => forall (x y : A), R x y -> R' (`f x) (`g y)).
 
@@ -93,12 +86,6 @@ Program Instance [ Equivalence A (R : relation A), Equivalence B (R' : relation
 
 Ltac obligations_tactic ::= program_simpl ; simpl_relation.
 
-Program Instance notT_arrow_morphism : 
-  Morphism (Type -> Type) (arrow ---> arrow) (fun X : Type => X -> False).
-
-Program Instance not_iso_morphism : 
-  Morphism (Type -> Type) (iso +++> iso) (fun X : Type => X -> False).
-
 Program Instance not_impl_morphism :
   Morphism (Prop -> Prop) (impl --> impl) not.
 
@@ -134,7 +121,7 @@ Program Instance `A` (R : relation A) `B` (R' : relation B)
     destruct respect with x y x0 y0 ; auto.
   Qed.
 
-Program Instance `A` (R : relation A) `B` (R' : relation B)
+Program Instance (A : Type) (R : relation A) `B` (R' : relation B)
   [ ? Morphism (R ++> R' ++> iff) m ] =>
   iff_inverse_impl_binary_morphism : ? Morphism (R ++> R' ++> inverse impl) m.
 
@@ -171,7 +158,7 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
 (* Definition respectful' A (R : relation A) B (R' : relation B) (f : A -> B) : relation A := *)
 (*   fun x y => R x y -> R' (f x) (f y). *)
 
-(* Definition morphism_respectful' A (R : relation A) B (R' : relation B) (f : A -> B) *)
+(* Definition morphism_respectful' A R B (R' : relation B) (f : A -> B) *)
 (*   [ ? Morphism (R ++> R') f ] (x y : A) : respectful' R R' f x y. *)
 (* intros. *)
 (* destruct H. *)
@@ -182,7 +169,7 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
 
 (* Existing Instance morphism_respectful'. *)
 
-(* Goal forall A [ Equivalence A (eqA : relation A) ] (R : relation A) [ ? Morphism (eqA ++> iff) m ] (x y : A)  *)
+(* Goal forall A [ Equivalence A (eqA : relation A) ] R [ ? Morphism (eqA ++> iff) m ] (x y : A)  *)
 (*   [ ? Morphism (eqA ++> eqA) m' ] (m' : A -> A), eqA x y -> True. *)
 (*   intros. *)
 (*   cut (relation A) ; intros R'. *)
@@ -210,7 +197,7 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
 
 (** A proof of [R x x] is available. *)
 
-(* Program Instance (A : Type) (R : relation A) B (R' : relation B) *)
+(* Program Instance (A : Type) R B (R' : relation B) *)
 (*   [ ? Morphism (R ++> R') m ] [ ? Morphism R x ] => *)
 (*   morphism_partial_app_morphism : ? Morphism R' (m x). *)
 
@@ -223,7 +210,7 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
 
 (** Morpshism declarations for partial applications. *)
 
-Program Instance [ Transitive A (R : relation A) ] (x : A) =>
+Program Instance [ Transitive A R ] (x : A) =>
   trans_contra_inv_impl_morphism : ? Morphism (R --> inverse impl) (R x).
 
   Next Obligation.
@@ -231,7 +218,7 @@ Program Instance [ Transitive A (R : relation A) ] (x : A) =>
     trans y...
   Qed.
 
-Program Instance [ Transitive A (R : relation A) ] (x : A) =>
+Program Instance [ Transitive A R ] (x : A) =>
   trans_co_impl_morphism : ? Morphism (R ++> impl) (R x).
 
   Next Obligation.
@@ -239,7 +226,7 @@ Program Instance [ Transitive A (R : relation A) ] (x : A) =>
     trans x0...
   Qed.
 
-Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) =>
+Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
   trans_sym_co_inv_impl_morphism : ? Morphism (R ++> inverse impl) (R x).
 
   Next Obligation.
@@ -248,7 +235,7 @@ Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) =>
     sym...
   Qed.
 
-Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) =>
+Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
   trans_sym_contra_impl_morphism : ? Morphism (R --> impl) (R x).
 
   Next Obligation.
@@ -257,7 +244,7 @@ Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) =>
     sym...
   Qed.
 
-Program Instance [ Equivalence A (R : relation A) ] (x : A) =>
+Program Instance [ Equivalence A R ] (x : A) =>
   equivalence_partial_app_morphism : ? Morphism (R ++> iff) (R x).
 
   Next Obligation.
@@ -270,7 +257,7 @@ Program Instance [ Equivalence A (R : relation A) ] (x : A) =>
 
 (** With symmetric relations, variance is no issue ! *)
 
-Program Instance [ Symmetric A (R : relation A) ] B (R' : relation B) 
+Program Instance [ Symmetric A R ] B (R' : relation B) 
   [ Morphism _ (R ++> R') m ] => 
   sym_contra_morphism : ? Morphism (R --> R') m.
 
@@ -282,7 +269,7 @@ Program Instance [ Symmetric A (R : relation A) ] B (R' : relation B)
 
 (** [R] is reflexive, hence we can build the needed proof. *)
 
-Program Instance [ Reflexive A (R : relation A) ] B (R' : relation B)
+Program Instance [ Reflexive A R ] B (R' : relation B)
   [ ? Morphism (R ++> R') m ] (x : A) =>
   reflexive_partial_app_morphism : ? Morphism R' (m x).
 
@@ -295,7 +282,7 @@ Program Instance [ Reflexive A (R : relation A) ] B (R' : relation B)
 
 (** Every symmetric and transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance [ Transitive A (R : relation A), Symmetric A R ] => 
+Program Instance [ Transitive A R, Symmetric A R ] => 
   trans_sym_morphism : ? Morphism (R ++> R ++> iff) R.
 
   Next Obligation.
@@ -306,7 +293,7 @@ Program Instance [ Transitive A (R : relation A), Symmetric A R ] =>
     trans y... trans y0... sym...
   Qed.
 
-Program Instance [ Equivalence A (R : relation A) ] => 
+Program Instance [ Equivalence A R ] => 
   equiv_morphism : ? Morphism (R ++> R ++> iff) R.
 
   Next Obligation.
@@ -335,16 +322,16 @@ Program Instance inverse_iff_impl_id :
 
 (** Logical conjunction. *)
 
-(* Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and. *)
+Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and.
 
-(* Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and. *)
+Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and.
 
 Program Instance and_iff_morphism : ? Morphism (iff ++> iff ++> iff) and.
 
 (** Logical disjunction. *)
 
-(* Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or. *)
+Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or.
 
-(* Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or. *)
+Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or.
 
 Program Instance or_iff_morphism : ? Morphism (iff ++> iff ++> iff) or.
diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v
index aaeb186545..9cc78a970d 100644
--- a/theories/Classes/Relations.v
+++ b/theories/Classes/Relations.v
@@ -22,41 +22,35 @@ Require Import Coq.Classes.Init.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Definition relationT A := A -> A -> Type.
-Definition relation A := A -> A -> Prop.
+Notation "'relation' A " := (A -> A -> Prop) (at level 0).
 
 Definition inverse A (R : relation A) : relation A := fun x y => R y x.
 
 Lemma inverse_inverse : forall A (R : relation A), inverse (inverse R) = R.
 Proof. intros ; unfold inverse. apply (flip_flip R). Qed.
 
-Definition complementT A (R : relationT A) := fun x y => notT (R x y).
-
 Definition complement A (R : relation A) := fun x y => R x y -> False.
 
 (** These are convertible. *)
 
-Lemma complementT_flip : forall A (R : relationT A), complementT (flip R) = flip (complementT R).
-Proof. reflexivity. Qed.
-
 Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R).
 Proof. reflexivity. Qed.
 
 (** We rebind relations in separate classes to be able to overload each proof. *)
 
-Class Reflexive A (R : relationT A) :=
+Class Reflexive A (R : relation A) :=
   reflexive : forall x, R x x.
 
-Class Irreflexive A (R : relationT A) := 
+Class Irreflexive A (R : relation A) := 
   irreflexive : forall x, R x x -> False.
 
-Class Symmetric A (R : relationT A) := 
+Class Symmetric A (R : relation A) := 
   symmetric : forall x y, R x y -> R y x.
 
-Class Asymmetric A (R : relationT A) := 
+Class Asymmetric A (R : relation A) := 
   asymmetric : forall x y, R x y -> R y x -> False.
 
-Class Transitive A (R : relationT A) := 
+Class Transitive A (R : relation A) := 
   transitive : forall x y z, R x y -> R y z -> R x z.
 
 Implicit Arguments Reflexive [A].
@@ -141,23 +135,6 @@ Ltac simpl_relation :=
 
 Ltac obligations_tactic ::= simpl_relation.
 
-(** The arrow is a reflexive and transitive relation on types. *)
-
-Program Instance arrow_refl : ? Reflexive arrow := 
-  reflexive X := id.
-
-Program Instance arrow_trans : ? Transitive arrow := 
-  transitive X Y Z f g := g o f.
-
-(** Isomorphism. *)
-
-Definition iso (A B : Type) := 
-  A -> B * B -> A.
-
-Program Instance iso_refl : ? Reflexive iso.
-Program Instance iso_sym : ? Symmetric iso.
-Program Instance iso_trans : ? Transitive iso.
-
 (** Logical implication. *)
 
 Program Instance impl_refl : ? Reflexive impl.
@@ -180,7 +157,7 @@ Program Instance eq_trans : ? Transitive (@eq A).
    - a tactic to immediately solve a goal without user intervention
    - a tactic taking input from the user to make progress on a goal *)
 
-Definition relate A (R : relationT A) : relationT A := R.
+Definition relate A (R : relation A) : relation A := R.
 
 Ltac relationify_relation R R' :=
   match goal with
@@ -287,7 +264,7 @@ Ltac relation_tac := relation_refl || relation_sym || relation_trans.
 
 (** The [PER] typeclass. *)
 
-Class PER (carrier : Type) (pequiv : relationT carrier) :=
+Class PER (carrier : Type) (pequiv : relation carrier) :=
   per_sym :> Symmetric pequiv ;
   per_trans :> Transitive pequiv.
 
@@ -307,14 +284,14 @@ Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] =>
 
 (** The [Equivalence] typeclass. *)
 
-Class Equivalence (carrier : Type) (equiv : relationT carrier) :=
+Class Equivalence (carrier : Type) (equiv : relation carrier) :=
   equiv_refl :> Reflexive equiv ;
   equiv_sym :> Symmetric equiv ;
   equiv_trans :> Transitive equiv.
 
 (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
 
-Class [ Equivalence A eqA ] => Antisymmetric (R : relationT A) := 
+Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := 
   antisymmetric : forall x y, R x y -> R y x -> eqA x y.
 
 Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq R ] => 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 5e18ef2aff..8c8c8c67c7 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -31,9 +31,10 @@ Class Setoid A :=
   equiv : relation A ;
   setoid_equiv :> Equivalence A equiv.
 
-Program Instance [ eqa : Equivalence A (eqA : relation A) ] => 
-  equivalence_setoid : Setoid A :=
-  equiv := eqA ; setoid_equiv := eqa.
+(* Too dangerous instance *)
+(* Program Instance [ eqa : Equivalence A eqA ] =>  *)
+(*   equivalence_setoid : Setoid A := *)
+(*   equiv := eqA ; setoid_equiv := eqa. *)
 
 (** Shortcuts to make proof search easier. *)
 
@@ -46,6 +47,10 @@ Proof. eauto with typeclass_instances. Qed.
 Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
 Proof. eauto with typeclass_instances. Qed.
 
+Existing Instance setoid_refl.
+Existing Instance setoid_sym.
+Existing Instance setoid_trans.
+
 (** Standard setoids. *)
 
 (* Program Instance eq_setoid : Setoid A := *)
@@ -142,11 +147,10 @@ Ltac obligations_tactic ::= morphism_tac.
 
 Program Instance iff_impl_id_morphism : ? Morphism (iff ++> impl) id.
 
-Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id.
+(* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *)
 
 (* Definition compose_respect (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
 (*   (x y : A -> C) : Prop := forall (f : A -> B) (g : B -> C), R f f -> R' g g. *)
-    
 
 (* Program Instance (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
 (*   [ mg : ? Morphism R' g ] [ mf : ? Morphism R f ] =>  *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 959dc10404..1d5280a490 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -34,7 +34,8 @@ open Entries
 let hint_db = "typeclass_instances"
 
 let add_instance_hint inst = 
-  Auto.add_hints false [hint_db] (Vernacexpr.HintsResolve [CRef (Ident (dummy_loc, inst))])
+  Auto.add_hints false [hint_db] 
+    (Vernacexpr.HintsResolve [CAppExpl (dummy_loc, (None, Ident (dummy_loc, inst)), [])])
 
 let declare_instance (_,id) =
   add_instance_hint id