diff options
Diffstat (limited to 'tactics/eauto.ml')
| -rw-r--r-- | tactics/eauto.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 239661498..f5c6ab879 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -178,7 +178,8 @@ and e_my_find_search sigma db_list local_db secvars hdc concl = | Extern tacast -> conclPattern concl p tacast in let tac = run_hint t tac in - (tac, lazy (pr_hint t))) + let sigma, env = Pfedit.get_current_context () in + (tac, lazy (pr_hint env sigma t))) in List.map tac_of_hint hintl |