From 2a384d9b4ea4b6de87d2d5a2a7259425589643cb Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 28 Jan 2010 16:05:55 +0000
Subject: Fix implicit_application for let-bound variables in the class
 context.

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

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 123998411b..d5894b208c 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -226,6 +226,7 @@ let combine_params avoid fn applied needed =
     (fun x -> match x with (t, Some (loc, ExplByName id)) -> id, t | _ -> assert false)
     named
   in
+  let needed = List.filter (fun (_, (_, b, _)) -> b = None) needed in
   let rec aux ids avoid app need =
     match app, need with
 	[], [] -> List.rev ids, avoid
-- 
cgit v1.2.3