Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

1 files changed, 16 insertions, 16 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 1c15fa40..e11458c0 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -17,7 +17,6 @@ open Proof_type
 open Tacticals
 open Tacmach
 open Tactics
-open Patternops
 open Clenv
 open Typeclasses
 open Globnames
@@ -42,7 +41,7 @@ let get_typeclasses_dependency_order () = !typeclasses_dependency_order
 
 open Goptions
 
-let set_typeclasses_modulo_eta =
+let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
@@ -51,7 +50,7 @@ let set_typeclasses_modulo_eta =
       optread  = get_typeclasses_modulo_eta;
       optwrite = set_typeclasses_modulo_eta; }
 
-let set_typeclasses_dependency_order =
+let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
@@ -222,20 +221,19 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
   in
   let tac_of_hint =
     fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) ->
-      let tac =
-	match t with
-	  | Res_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_resolve poly flags)
-	  | ERes_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_e_resolve poly flags)
-	  | Give_exact c -> e_give_exact flags poly c
-	  | Res_pf_THEN_trivial_fail (term,cl) ->
-              tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
-	        (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)
-	  | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c])
-	  | Extern tacast ->
-	    Proofview.V82.of_tactic (conclPattern concl p tacast)
+      let tac = function
+      | Res_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_resolve poly flags))
+      | ERes_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
+      | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c)
+      | Res_pf_THEN_trivial_fail (term,cl) ->
+          Proofview.V82.tactic (tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
+            (if complete then tclIDTAC else e_trivial_fail_db db_list local_db))
+      | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c]))
+      | Extern tacast -> conclPattern concl p tacast
       in
+      let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in
       let tac = if complete then tclCOMPLETE tac else tac in
-	match t with
+	match repr_auto_tactic t with
 	| Extern _ -> (tac,b,true, name, lazy (pr_autotactic t))
 	| _ ->
 (* 	  let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *)
@@ -351,7 +349,9 @@ let make_autogoal_hints =
       let sign = pf_filtered_hyps g in
       let (onlyc, sign', cached_hints) = !cache in
 	if onlyc == only_classes && 
-	  (sign == sign' || Environ.eq_named_context_val sign sign') then
+	  (sign == sign' || Environ.eq_named_context_val sign sign') 
+	  && Hint_db.transparent_state cached_hints == st
+	then
 	  cached_hints
 	else
 	  let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in