diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 19:08:35 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-21 18:04:32 +0100 |
| commit | 0ddf7d9c35eb2dd5f368e7a5735970ef1fd41fc6 (patch) | |
| tree | 0bc32293ac19ddd63cf764ccbd224b086c7836bc /tactics/autorewrite.ml | |
| parent | b75beb248873db7d9ab8e4a078022b2ed0edcd36 (diff) | |
[printing] Deprecate all printing functions accessing the global proof.
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index e68087f14..6a9cd7e20 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -74,12 +74,12 @@ let find_matches bas pat = let res = HintDN.search_pattern base pat in List.map snd res -let print_rewrite_hintdb bas = +let print_rewrite_hintdb env sigma bas = (str "Database " ++ str bas ++ fnl () ++ prlist_with_sep fnl (fun h -> str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++ - Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++ + Printer.pr_lconstr_env env sigma h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr_env env sigma h.rew_type ++ Option.cata (fun tac -> str " then use tactic " ++ Pputils.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac) (find_rewrites bas)) |