diff options
| author | Hugo Herbelin | 2014-10-07 17:26:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-07 18:40:36 +0200 |
| commit | 38b34dfffcceab7fa7d5ba43c84e414d24cebe43 (patch) | |
| tree | c5449cf9c02c97586bf8a8edaa52d05d876d3e94 /tactics/class_tactics.ml | |
| parent | 2313bde0116a5916912bebbaca77d291f7b2760a (diff) | |
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
being able to export hints without tactics, vm, etc. to come with.
Some functions moved to the new proof engine.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index d9f90b02e6..38f1114b52 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -25,6 +25,7 @@ open Evd open Locus open Misctypes open Proofview.Notations +open Hints (** Hint database named "typeclass_instances", now created directly in Auto *) @@ -215,7 +216,7 @@ let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) evs (Evarutil.nf_ let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l) -type autoinfo = { hints : Auto.hint_db; is_evar: existential_key option; +type autoinfo = { hints : hint_db; is_evar: existential_key option; only_classes: bool; unique : bool; auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t; auto_path : global_reference option list; @@ -750,7 +751,7 @@ let set_typeclasses_depth = let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl = try let dbs = List.map_filter - (fun db -> try Some (Auto.searchtable_map db) + (fun db -> try Some (searchtable_map db) with e when Errors.noncritical e -> None) dbs in @@ -787,7 +788,7 @@ let is_ground c gl = let autoapply c i gl = let flags = auto_unif_flags Evar.Set.empty - (Auto.Hint_db.transparent_state (Auto.searchtable_map i)) in + (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in let cty = pf_type_of gl c in let ce = mk_clenv_from gl (c,cty) in unify_e_resolve false flags (c,ce) gl |