diff options
| author | filliatr | 2002-02-08 15:41:18 +0000 |
|---|---|---|
| committer | filliatr | 2002-02-08 15:41:18 +0000 |
| commit | 748c2c5c6f4d2d5f0b8799d120891d4bb7833fb4 (patch) | |
| tree | 65866955c2c52afb5aa25f838fe7b51b613988b9 | |
| parent | d2a0862f34c51dd52db6be34ae1cf60a590c4e9a (diff) | |
prterm -> prterm_env
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2463 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |