Fix handling of instance declarations in presence of let-ins (bug

reported by Eelis van der Weegen).


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

2 files changed, 32 insertions, 23 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 96e36b70ba..8d987d0379 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -272,7 +272,8 @@ let class_info c =
   with _ -> not_a_class (Global.env()) (constr_of_global c)
 
 let instance_constructor cl args =
-  let pars = fst (list_chop (List.length (fst cl.cl_context)) args) in
+  let lenpars = List.length (List.filter (fun (na, b, t) -> b = None) (snd cl.cl_context)) in
+  let pars = fst (list_chop lenpars args) in
     match cl.cl_impl with
       | IndRef ind -> applistc (mkConstruct (ind, 1)) args,
 	  applistc (mkInd ind) pars
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 5eabc852d8..a45ab88606 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -80,19 +80,18 @@ let interp_type_evars evdref env ?(impls=empty_internalization_env) typ =
 open Topconstr
 
 let type_ctx_instance evars env ctx inst subst =
-  let (s, _) =
-    List.fold_left2
-      (fun (subst, instctx) (na, b, t) ce ->
-	let t' = substl subst t in
-	let c' =
-	  match b with
-	  | None -> interp_casted_constr_evars evars env ce t'
-	  | Some b -> substl subst b
-	in
-	let d = na, Some c', t' in
-	  c' :: subst, d :: instctx)
-      (subst, []) (List.rev ctx) inst
-  in s
+  let rec aux (subst, instctx) l = function
+    (na, b, t) :: ctx ->
+      let t' = substl subst t in
+      let c', l =
+	match b with
+	| None -> interp_casted_constr_evars evars env (List.hd l) t', List.tl l
+	| Some b -> substl subst b, l
+      in
+      let d = na, Some c', t' in
+	aux (c' :: subst, d :: instctx) l ctx
+    | [] -> subst
+  in aux (subst, []) inst (List.rev ctx)
 
 let refine_ref = ref (fun _ -> assert(false))
 
@@ -155,7 +154,14 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
     let ctx', c = decompose_prod_assum c' in
     let ctx'' = ctx' @ ctx in
     let cl, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in
-      cl, c', ctx', ctx, len, imps, List.rev args
+    let _, args = 
+      List.fold_right (fun (na, b, t) (args, args') ->
+	match b with
+	| None -> (List.tl args, List.hd args :: args')
+	| Some b -> (args, b :: args'))
+	(snd cl.cl_context) (args, [])
+    in
+      cl, c', ctx', ctx, len, imps, args
   in
   let id =
     match snd instid with
@@ -209,14 +215,16 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 	      let props, rest =
 		List.fold_left
 		  (fun (props, rest) (id,b,_) ->
-		    try
-		      let (loc_mid, c) = List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest in
-		      let rest' = List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest in
-		      let (loc, mid) = get_id loc_mid in
-			Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
-			c :: props, rest'
-		    with Not_found ->
-		      (CHole (Util.dummy_loc, None) :: props), rest)
+		    if b = None then
+		      try
+			let (loc_mid, c) = List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest in
+			let rest' = List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest in
+			let (loc, mid) = get_id loc_mid in
+			  Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
+			  c :: props, rest'
+		      with Not_found ->
+			(CHole (Util.dummy_loc, None) :: props), rest
+		    else props, rest)
 		  ([], props) k.cl_props
 	      in
 		if rest <> [] then