From aab16ea645fefd71b6bd0fdb155a076640ab0d4e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 2 Aug 2010 21:14:19 +0000
Subject: Fix [clenv_missing] to compute a better approximation of missing
 dependent arguments. It breaks compatibility as some [apply with] clauses are
 not necessary anymore. Typically when applying [f_equal], the domain type of
 the function can be infered even if it does not appear directly in the
 conclusion of the goal. Fixes bug #2154.

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

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index ca77e10c8d..a8b13e8456 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -229,6 +229,7 @@ let clenv_dependent hyps_only clenv =
   let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
   let deps = dependent_metas clenv mvs ctyp_mvs in
   let nonlinear = duplicated_metas (clenv_value clenv) in
+  let ctyp_mvs = dependent_metas clenv (Metaset.elements ctyp_mvs) ctyp_mvs in
   (* Make the assumption that duplicated metas have internal dependencies *)
   List.filter
     (fun mv -> if Metaset.mem mv deps
-- 
cgit v1.2.3