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/eauto.ml | |
| parent | b409b9837ce438042bb259d16a1b5156a2e0acb9 (diff) | |
Dnets now consider axioms as being opaque for pattern recognition.
Diffstat (limited to 'tactics/eauto.ml')
| -rw-r--r-- | tactics/eauto.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 17e6a6edb4..e920093648 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -67,7 +67,7 @@ open Auto let unify_e_resolve flags h = Hints.hint_res_pf ~with_evars:true ~with_classes:true ~flags h -let hintmap_of sigma secvars concl = +let hintmap_of env sigma secvars concl = (* Warning: for computation sharing, we need to return a closure *) let hdc = try Some (decompose_app_bound sigma concl) with Bound -> None in match hdc with @@ -78,7 +78,7 @@ let hintmap_of sigma secvars concl = match Hint_db.map_existential sigma ~secvars hdc concl db with | ModeMatch l -> l | ModeMismatch -> []) - else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db) + else (fun db -> Hint_db.map_auto env sigma ~secvars hdc concl db) (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) let e_exact flags h = @@ -106,7 +106,7 @@ let rec e_trivial_fail_db db_list local_db = end and e_my_find_search env sigma db_list local_db secvars concl = - let hint_of_db = hintmap_of sigma secvars concl in + let hint_of_db = hintmap_of env sigma secvars concl in let hintl = List.map_append (fun db -> let flags = auto_flags_of_state (Hint_db.transparent_state db) in |