From 562c684cd19c37e04901743c73933ea12148940b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 9 Oct 2009 22:21:30 +0000
Subject: Fix bug #2162 and a name clashing bug in generalized binders.

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

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 7b1a1ff4cc..a55daff364 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -225,7 +225,7 @@ let implicit_application env ?(allow_partial=true) f ty =
     with Not_found -> None
   in
     match is_class with
-    | None -> ty
+    | None -> ty, env
     | Some ((loc, id, par), gr) ->
 	let avoid = Idset.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
 	let c, avoid =
@@ -241,7 +241,7 @@ let implicit_application env ?(allow_partial=true) f ty =
 	  let pars = List.rev (List.combine ci rd) in
 	  let args, avoid = combine_params avoid f par pars in
 	    CAppExpl (loc, (None, id), args), avoid
-	in c
+	in c, avoid
 
 let implicits_of_rawterm l =
   let rec aux i c =
-- 
cgit v1.2.3