diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-11 16:13:58 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:55:46 +0200 |
| commit | 9e038688af8f7f054c1c2acdb2fe65d78cccdd81 (patch) | |
| tree | 5191db2f8740db49fd7d9fb60878431de17b9ea7 /printing/ppconstr.ml | |
| parent | 2211eeda012477b26081738fccc59aa31fb0a565 (diff) | |
Temporary deactivate re-interpretation of terms in beautify.
Diffstat (limited to 'printing/ppconstr.ml')
| -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 7fad6fb9a..56fbdd5ff 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 |