From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 13 Feb 2007 13:48:12 +0000
Subject: Imported Upstream version 8.1+dfsg

---
 ide/coq.ml | 16 ++--------------
 1 file changed, 2 insertions(+), 14 deletions(-)

(limited to 'ide')

diff --git a/ide/coq.ml b/ide/coq.ml
index fae34ef2..6059f065 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq.ml 9263 2006-10-23 12:08:08Z barras $ *)
+(* $Id: coq.ml 9537 2007-01-26 10:05:04Z corbinea $ *)
 
 open Vernac
 open Vernacexpr
@@ -269,18 +269,6 @@ let prepare_goal sigma g =
   (prepare_hyps sigma env,
    (env, sigma, g.evar_concl, msg (pr_ltype_env_at_top env g.evar_concl)))
 
-let prepare_hyps_filter info sigma env =
-  assert (rel_context env = []);
-  let hyps =
-    fold_named_context
-      (fun env ((id,_,_) as d) acc ->
-	 if true || Idset.mem id info.pm_hyps then
-	   let hyp = prepare_hyp sigma env d in hyp :: acc
-	 else acc)
-      env ~init:[] 
-  in
-  List.rev hyps
-
 let prepare_meta sigma env (m,typ)  =
   env, sigma, 
   (msg (str " ?" ++ int m ++ str " : " ++ pr_ltype_env_at_top env typ))
@@ -297,7 +285,7 @@ let get_current_pm_goal () =
   let info = Decl_mode.get_info gls.it in
   let env = pf_env gls in
   let sigma= sig_sig gls in
-    (prepare_hyps_filter info sigma env,
+    (prepare_hyps sigma env,
      prepare_metas info sigma env)
 
 let get_current_goals () = 
-- 
cgit v1.2.3