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
---
 proofs/goal.ml  | 5 -----
 proofs/goal.mli | 3 ---
 2 files changed, 8 deletions(-)

(limited to 'proofs')

diff --git a/proofs/goal.ml b/proofs/goal.ml
index a2efc10f02..6cd00c3188 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -466,11 +466,6 @@ module V82 = struct
     let evi = content evars gl in
     Evd.evar_filtered_env evi
 
-  (* For printing *)
-  let unfiltered_env evars gl =
-    let evi = content evars gl in
-    Evd.evar_env evi
-
   (* Old style hyps primitive *)
   let hyps evars gl =
     let evi = content evars gl in
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 72f1b16a46..49667879b4 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -182,9 +182,6 @@ module V82 : sig
   (* Old style env primitive *)
   val env : Evd.evar_map -> goal -> Environ.env
 
-  (* For printing *)
-  val unfiltered_env : Evd.evar_map -> goal -> Environ.env
-
   (* Old style hyps primitive *)
   val hyps : Evd.evar_map -> goal -> Environ.named_context_val
 
-- 
cgit v1.2.3