diff options
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 32 |
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 |