diff options
| author | Pierre-Marie Pédrot | 2015-05-05 00:20:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-05 00:20:54 +0200 |
| commit | 34e6a7149a69791cc736bdd9b2b909be9f21ec8f (patch) | |
| tree | f33a4ed37d7fff96df7a720fe6146ecce56aba81 /printing/printer.ml | |
| parent | 72644c7f7b3f0fcc56779acfcfa4bfc9f041ebde (diff) | |
| parent | df54c829a4c06a93de47df4e8ccc441721360da8 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 0d3a1c17e4..141ae145dd 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -654,7 +654,7 @@ let pr_goal_by_id id = let p = Proof_global.give_me_the_proof () in let g = Goal.get_by_uid id in let pr gs = - v 0 (str ("goal / evar " ^ id ^ " is:") ++ cut () + v 0 (str "goal / evar " ++ str id ++ str " is:" ++ cut () ++ pr_goal gs) in try @@ -723,7 +723,7 @@ let pr_assumptionset env s = try pr_constant env kn with Not_found -> let mp,_,lab = repr_con kn in - str (string_of_mp mp ^ "." ^ Label.to_string lab) + str (string_of_mp mp) ++ str "." ++ pr_label lab in let safe_pr_ltype typ = try str " : " ++ pr_ltype typ |