From f907cc977bb80e3654174de03aeaed2cb4aa4a7e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 15 Apr 2008 16:35:54 +0000
Subject: Mises à jour bugs, CHANGES, code mort

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10801 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/clenv.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 072d664fcd..ed9d779ad7 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -231,7 +231,6 @@ let dependent_metas clenv mvs conclmetas =
     mvs conclmetas
 
 let clenv_dependent hyps_only clenv =
-  let mvs = collect_metas (clenv_value clenv) in
   let mvs = undefined_metas clenv.evd in
   let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
   let deps = dependent_metas clenv mvs ctyp_mvs in
-- 
cgit v1.2.3