From 1fe47f95097b0245081a4feb4a5d44f761301dca Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 5 Aug 2014 15:20:35 +0200
Subject: Preliminary re-installation of notation interpretation in beautifying
 mode.

---
 printing/ppconstr.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 2aae3ebb60..b38cfa664c 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -583,6 +583,14 @@ let modular_constr_pr = pr
 let rec fix rf x =rf (fix rf) x
 let pr = fix modular_constr_pr mt
 
+let transf env c =
+  if !Flags.beautify_file then
+    let r = Constrintern.for_grammar (Constrintern.intern_constr env) c in
+    Constrextern.extern_glob_constr (Termops.vars_of_env env) r
+  else c
+
+let pr prec c = pr prec (transf (Global.env()) c)
+
 let pr_simpleconstr = function
   | CAppExpl (_,(None,f,us),[]) -> str "@" ++ pr_cref f us
   | c -> pr lsimpleconstr c
-- 
cgit v1.2.3