decl mode: anonymous facts

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9534 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 13 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 17965558c..a7d8da813 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -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 () =