diff options
| -rw-r--r-- | proofs/logic.ml | 2 | ||||
| -rw-r--r-- | proofs/refiner.ml | 3 |
2 files changed, 4 insertions, 1 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 5e920ea5ac..23b512bcbe 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -703,6 +703,8 @@ let prim_extractor subfun vl pft = open Printer +let prterm x = prterm_env (Global.env()) x + let pr_prim_rule = function | {name=Intro;newids=[id]} -> str"Intro " ++ pr_id id diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 6806cf2b6b..7937b9913e 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -829,7 +829,8 @@ let rec print_proof sigma osign pf = hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl) ) -let pr_change gl = (str"Change " ++ prterm gl.evar_concl ++ str"." ++ fnl ()) +let pr_change gl = + (str"Change " ++ prterm_env (Global.env()) gl.evar_concl ++ str"." ++ fnl ()) let rec print_script nochange sigma osign pf = let {evar_hyps=sign; evar_concl=cl} = pf.goal in |