From 4f02527d87b20bbdb8d8044097fe39c4191ed126 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 19 Dec 2002 14:09:05 +0000
Subject: bug: Global.env() executé au chargement -> eta-expansion

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3459 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/printer.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 7777ac5402..72fe499e67 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -39,14 +39,14 @@ let tactic_initial_prec = Some ((tactic_syntax_universe,(9,0,0)),Ppextend.L)
 
 let prterm_env_at_top env = gentermpr_core true env
 let prterm_env env = gentermpr_core false env
-let prterm = prterm_env (Global.env())
-
 let prtype_env env typ = prterm_env env typ
-let prtype = prtype_env (Global.env())
-
 let prjudge_env env j =
   (prterm_env env j.uj_val, prterm_env env j.uj_type)
-let prjudge = prjudge_env (Global.env())
+
+(* NB do not remove the eta-redexes! Global.env() has side-effects... *)
+let prterm t = prterm_env (Global.env()) t
+let prtype t = prtype_env (Global.env()) t
+let prjudge j = prjudge_env (Global.env()) j
 
 let fprterm_env a =
   warning "Fw printing not implemented, use CCI printing 1"; prterm_env a
-- 
cgit v1.2.3