diff options
| author | Hugo Herbelin | 2016-04-27 22:13:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 22:13:04 +0200 |
| commit | 2cc594d270aae473228c7e1301d042eea38061da (patch) | |
| tree | 2a60a63a50818a970f5639570ed27b5843c2e88e | |
| parent | a6fa936bbd0c4367b7a4d87df786645c138327b3 (diff) | |
Revert "Temporary deactivate re-interpretation of terms in beautify."
This reverts commit 9e038688af8f7f054c1c2acdb2fe65d78cccdd81.
| -rw-r--r-- | printing/ppconstr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 56fbdd5ff5..7fad6fb9ab 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -712,7 +712,7 @@ end) = struct Constrextern.extern_glob_constr (Termops.vars_of_env env) r else c - let pr prec c = pr prec ((*transf (Global.env())*) c) + let pr prec c = pr prec (transf (Global.env()) c) let pr_simpleconstr = function | CAppExpl (_,(None,f,us),[]) -> str "@" ++ pr_cref f us |