From ea1d98ba6e64572cb9469c76bd6a51d74fb08ce1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 29 Jan 2013 18:15:21 +0000
Subject: No reason a priori for using unfiltered env for printing goal.
 Filtered env is intended to be type-safe.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16177 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/decl_mode/g_decl_mode.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 0b7e94fa0b..70338c52b5 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -22,7 +22,7 @@ open Pcoq.Tactic
 
 let pr_goal gs =
   let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in
-  let env = Goal.V82.unfiltered_env sigma g in
+  let env = Goal.V82.env sigma g in
   let preamb,thesis,penv,pc =
     (str "     *** Declarative Mode ***" ++ fnl ()++fnl ()),
     (str "thesis := "  ++ fnl ()),
-- 
cgit v1.2.3