diff options
| author | Maxime Dénès | 2017-11-21 22:24:59 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-21 22:24:59 +0100 |
| commit | eb91ccaf236bc9a60a1e216b76a0a42980c072a7 (patch) | |
| tree | 0bc32293ac19ddd63cf764ccbd224b086c7836bc /tactics/auto.ml | |
| parent | b75beb248873db7d9ab8e4a078022b2ed0edcd36 (diff) | |
| parent | 0ddf7d9c35eb2dd5f368e7a5735970ef1fd41fc6 (diff) | |
Merge PR #6173: [printing] Deprecate all printing functions accessing the global proof.
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index d0424eb892..fa8435d1ff 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -388,7 +388,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db= Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) else Tacticals.New.tclFAIL 0 (str"Unbound reference") end - | Extern tacast -> + | Extern tacast -> conclPattern concl p tacast in let pr_hint () = @@ -396,7 +396,8 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db= | None -> mt () | Some n -> str " (in " ++ str n ++ str ")" in - pr_hint t ++ origin + let sigma, env = Pfedit.get_current_context () in + pr_hint env sigma t ++ origin in tclLOG dbg pr_hint (run_hint t tactic) |