3 files changed, 27 insertions, 6 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 3ab41c62b..8854ff898 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -151,7 +151,7 @@ let tag_var = tag Tag.variable
     str "`" ++ str hd ++ c ++ str tl
 
   let pr_com_at n =
-    if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n)
+    if !Flags.beautify && not (Int.equal n 0) then comment (Pputils.extract_comments n)
     else mt()
 
   let pr_with_comments ?loc pp = pr_located (fun x -> x) (loc, pp)
@@ -703,13 +703,16 @@ let tag_var = tag Tag.variable
     | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us
     | c -> pr prec c
 
-  let transf env c =
+  let transf env sigma c =
     if !Flags.beautify_file then
-      let r = Constrintern.for_grammar (Constrintern.intern_constr env) c in
+      let r = Constrintern.for_grammar (Constrintern.intern_constr env sigma) c in
       Constrextern.extern_glob_constr (Termops.vars_of_env env) r
     else c
 
-  let pr_expr prec c = pr prec (transf (Global.env()) c)
+  let pr_expr prec c =
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    pr prec (transf env sigma c)
 
   let pr_simpleconstr = pr_expr lsimpleconstr
 
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 6b23b7fe9..010b92f3e 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -15,14 +15,26 @@ open Misctypes
 open Locus
 open Genredexpr
 
+let beautify_comments = ref []
+
+let rec split_comments comacc acc pos = function
+  | [] -> beautify_comments := List.rev acc; comacc
+  | ((b,e),c as com)::coms ->
+      (* Take all comments that terminates before pos, or begin exactly
+         at pos (used to print comments attached after an expression) *)
+      if e<=pos || pos=b then split_comments (c::comacc) acc pos coms
+      else split_comments comacc (com::acc) pos coms
+
+let extract_comments pos = split_comments [] [] pos !beautify_comments
+
 let pr_located pr (loc, x) =
   match loc with
   | Some loc when !Flags.beautify ->
     let (b, e) = Loc.unloc loc in
     (* Side-effect: order matters *)
-    let before = Pp.comment (CLexer.extract_comments b) in
+    let before = Pp.comment (extract_comments b) in
     let x = pr x in
-    let after = Pp.comment (CLexer.extract_comments e) in
+    let after = Pp.comment (extract_comments e) in
     before ++ x ++ after
   | _ -> pr x
 
diff --git a/printing/pputils.mli b/printing/pputils.mli
index 06123362a..6039168f8 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -39,3 +39,9 @@ val pr_red_expr_env : Environ.env -> Evd.evar_map ->
 
 val pr_raw_generic : Environ.env -> rlevel generic_argument -> Pp.t
 val pr_glb_generic : Environ.env -> glevel generic_argument -> Pp.t
+
+(* The comments interface is imperative due to the printer not
+   threading it, this could be solved using a better data
+   structure. *)
+val beautify_comments : ((int * int) * string) list ref
+val extract_comments : int -> string list