From 2a75ae37ec90b1b80c960c498028f13f90b0047e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 24 Dec 2002 11:27:11 +0000
Subject: code mort

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

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 55e0fa5d37..80fccbf687 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -1092,14 +1092,6 @@ let clenv_pose_dependent_evars clenv =
 
 (***************************)
 
-let is_dependent clause =
-  match
-    kind_of_term (clenv_instance_template clause),
-    kind_of_term (clenv_instance_template_type clause)
-  with
-      App(f,l), App(g,l') when isMeta g & array_last l = array_last l' -> true
-    | _ -> false
-
 let clenv_unique_resolver allow_K clause gl =
   clenv_unify allow_K CUMUL
     (clenv_instance_template_type clause) (pf_concl gl) clause 
-- 
cgit v1.2.3