From 900d95913b625f9a7483dfefbf7ea0fbf93bcea2 Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 3 Sep 2004 18:56:25 +0000
Subject: deplacement de clenv vers pretyping

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

(limited to 'parsing/printer.ml')

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 477b7bf970..c331eea6fd 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -124,6 +124,8 @@ 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 _ = Termops.set_print_constr prterm
+
 let pr_constant env cst = prterm_env env (mkConst cst)
 let pr_existential env ev = prterm_env env (mkEvar ev)
 let pr_inductive env ind = prterm_env env (mkInd ind)
@@ -247,3 +249,4 @@ let pr_context_limit n env =
 let pr_context_of env = match Options.print_hyps_limit () with 
   | None -> hv 0 (pr_context_unlimited env)
   | Some n -> hv 0 (pr_context_limit n env)
+
-- 
cgit v1.2.3