diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:04 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 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 56fbdd5ff..7fad6fb9a 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 |