Do a fixpoint on the result of typeclass search to force the

resolution of generated evars, not doing any backtracking yet.


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

2 files changed, 12 insertions, 9 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 78ef3c6fc8..6fdd8c2827 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -217,7 +217,7 @@ type 'a tac = { skft : 'ans. ('a,'ans) sk -> 'ans fk -> autogoal sigma -> 'ans }
 type auto_result = autogoal list sigma * validation
 
 type atac = auto_result tac
-  
+
 let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac =
   { skft = fun sk fk {it = gl,hints; sigma=s} ->
     let res = try Some (tac {it=gl; sigma=s}) with e when catchable e -> None in
@@ -326,6 +326,7 @@ let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : auto_result o
 let rec fix (t : 'a tac) : 'a tac = 
   then_tac t { skft = fun sk fk -> (fix t).skft sk fk }
 
+  
 (* A special one for getting everything into a dnet. *)
 
 let is_transparent_gr (ids, csts) = function
@@ -357,10 +358,10 @@ let make_autogoals ?(st=full_transparent_state) gs evm' =
   { it = list_map_i (fun i g -> 
     let (gl, auto) = make_autogoal ~st {it = snd g; sigma = evm'} in
       (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm' }
-    
+
 let run_on_evars ?(st=full_transparent_state) p evm tac =
   match evars_to_goals p evm with
-  | None -> raise Not_found
+  | None -> None
   | Some (goals, evm') ->
       match run_list_tac tac p goals (make_autogoals ~st goals evm') with
       | None -> raise Not_found
@@ -379,13 +380,15 @@ let eauto hints g =
 
 let real_eauto st hints p evd =
   let tac = fix (hints_tac hints) in
-    run_on_evars ~st p evd tac
-      
+  let rec aux evd =
+    match run_on_evars ~st p evd tac with
+    | None -> evd
+    | Some evd' -> aux evd'
+  in aux evd
+
 let resolve_all_evars_once debug (mode, depth) p evd =
   let db = searchtable_map typeclasses_db in
-    match real_eauto (Hint_db.transparent_state db) [db] p evd with
-    | None -> raise Not_found
-    | Some res -> res
+    real_eauto (Hint_db.transparent_state db) [db] p evd
 
 exception FoundTerm of constr
 
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 9e1eecd1d3..595ad12975 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -325,7 +325,7 @@ Proof. firstorder. Qed.
 Lemma proper_proper_proxy `(Proper A R x) : ProperProxy R x.
 Proof. firstorder. Qed.
 
-Hint Extern 1 (ProperProxy _ _) => class_apply eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances.
+Hint Extern 1 (ProperProxy _ _) => class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances.
 Hint Extern 2 (ProperProxy ?R _) => not_evar R ; class_apply @proper_proper_proxy : typeclass_instances.
 
 (** [R] is Reflexive, hence we can build the needed proof. *)