Fix bug #1943 and restrict the inference optimisation of Program to

cases where coercion could not occur as well.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11414 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 2 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index d084a3f7d..8bacbcd8c 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -169,7 +169,9 @@ let full_class_binders env l =
 	    let gr = Nametab.global id in
 	      (try
 		  let c = class_info gr in
-		  let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in
+		  let (ci, rd) = c.cl_context in
+		  let pars = List.rev (List.combine ci rd) in
+		  let args, avoid = combine_params_freevar avoid l pars in
 		    (iid, bk, CAppExpl (loc, (None, id), args)) :: l', avoid
 		with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
 	| Explicit -> (x :: l', avoid))
@@ -206,7 +208,9 @@ let full_class_binder env (iid, (bk, bk'), cl as c) =
 	let gr = Nametab.global id in
 	  (try
 	      let c = class_info gr in
-	      let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in
+	      let (ci, rd) = c.cl_context in
+	      let pars = List.rev (List.combine ci rd) in
+	      let args, avoid = combine_params_freevar avoid l pars in
 		(iid, bk, CAppExpl (loc, (None, id), args)), avoid
 	    with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
     | Explicit -> ((iid,bk,cl), avoid)