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 /stm | |
| parent | b75beb248873db7d9ab8e4a078022b2ed0edcd36 (diff) | |
| parent | 0ddf7d9c35eb2dd5f368e7a5735970ef1fd41fc6 (diff) | |
Merge PR #6173: [printing] Deprecate all printing functions accessing the global proof.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 864fff9e0b..a9cbcc9a6d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1931,9 +1931,10 @@ end = struct (* {{{ *) let open Notations in match Future.join f with | Some (pt, uc) -> + let sigma, env = Pfedit.get_current_context () in stm_pperr_endline (fun () -> hov 0 ( str"g=" ++ int (Evar.repr gid) ++ spc () ++ - str"t=" ++ (Printer.pr_constr pt) ++ spc () ++ + str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++ str"uc=" ++ Termops.pr_evar_universe_context uc)); (if abstract then Tactics.tclABSTRACT None else (fun x -> x)) (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*> |