diff options
| author | Pierre-Marie Pédrot | 2020-06-22 12:59:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-20 11:47:34 +0200 |
| commit | 4ebccb9d2722a7323cb7fce5c9e00bf2eea5b69f (patch) | |
| tree | ca132eb8ef2d3a30b8addb7633d3b263a1cdfb38 /tactics/class_tactics.ml | |
| parent | b409b9837ce438042bb259d16a1b5156a2e0acb9 (diff) | |
Dnets now consider axioms as being opaque for pattern recognition.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 378a3e718b..2f55cc071f 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -257,13 +257,13 @@ let shelve_dependencies gls = Feedback.msg_debug (str" shelving dependent subgoals: " ++ pr_gls sigma gls); shelve_goals gls) -let hintmap_of sigma hdc secvars concl = +let hintmap_of env sigma hdc secvars concl = match hdc with | None -> fun db -> ModeMatch (Hint_db.map_none ~secvars db) | Some hdc -> fun db -> if Hint_db.use_dn db then (* Using dnet *) - Hint_db.map_eauto sigma ~secvars hdc concl db + Hint_db.map_eauto env sigma ~secvars hdc concl db else Hint_db.map_existential sigma ~secvars hdc concl db (** Hack to properly solve dependent evars that are typeclasses *) @@ -373,7 +373,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm | Extern _ -> (tac, b, true, name, lazy (FullHint.print env sigma h ++ pp)) | _ -> (tac, b, false, name, lazy (FullHint.print env sigma h ++ pp)) in - let hint_of_db = hintmap_of sigma hdc secvars concl in + let hint_of_db = hintmap_of env sigma hdc secvars concl in let hintl = List.map_filter (fun db -> match hint_of_db db with | ModeMatch l -> Some (db, l) | ModeMismatch -> None) |