summaryrefslogtreecommitdiff
path: root/tactics/class_tactics.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/class_tactics.ml')
-rw-r--r--tactics/class_tactics.ml32
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