diff options
| author | Hugo Herbelin | 2014-08-05 15:20:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-05 19:52:23 +0200 |
| commit | 1fe47f95097b0245081a4feb4a5d44f761301dca (patch) | |
| tree | 86c22453d1f8303f213d3c5c575d56949f934df2 /printing/ppconstr.ml | |
| parent | ac9f225940357ffd9841f1df277c4f78964df313 (diff) | |
Preliminary re-installation of notation interpretation in beautifying mode.
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 8 |
1 files changed, 8 insertions, 0 deletions
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 |