aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-27 22:13:04 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-27 22:13:04 +0200
commit2cc594d270aae473228c7e1301d042eea38061da (patch)
tree2a60a63a50818a970f5639570ed27b5843c2e88e
parenta6fa936bbd0c4367b7a4d87df786645c138327b3 (diff)
Revert "Temporary deactivate re-interpretation of terms in beautify."
-rw-r--r--printing/ppconstr.ml2
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