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

6 files changed, 12 insertions, 11 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c251ffb24..aa836ea11 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -697,8 +697,9 @@ let push_loc_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env)
 
 let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar
     (ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty =
-  let ty =
-    if t then ty else
+  let ids = match na with Anonymous -> ids | Name na -> Idset.add na ids in
+  let ty, ids' =
+    if t then ty, ids else
       Implicit_quantifiers.implicit_application ids
 	Implicit_quantifiers.combine_params_freevar ty
   in
@@ -715,7 +716,7 @@ let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar
 	      match ty with
 	      | CApp (_, (_, CRef (Ident (loc,id))), _) -> id
 	      | _ -> id_of_string "H"
-	    in Implicit_quantifiers.make_fresh ids (Global.env ()) id
+	    in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
 	  in Name name
     | _ -> na
   in (push_loc_name_env ~fail_anonymous lvar env' loc na), (na,b',None,ty') :: List.rev bl
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 7b1a1ff4c..a55daff36 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 =
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 57eff0b86..0d28eccad 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -51,4 +51,4 @@ val combine_params_freevar :
 val implicit_application : Idset.t -> ?allow_partial:bool ->
   (Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
     Topconstr.constr_expr * Names.Idset.t) ->
-  constr_expr -> constr_expr
+  constr_expr -> constr_expr * Idset.t
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 6fe14da34..93b65cd00 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -95,7 +95,7 @@ let substitution_of_constrs ctx cstrs =
 let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) pri =
   let env = Global.env() in
   let isevars = ref Evd.empty in
-  let tclass =
+  let tclass, _ =
     match bk with
     | Implicit ->
 	Implicit_quantifiers.implicit_application Idset.empty (* need no avoid *)
@@ -110,7 +110,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 		in t, avoid
 	    | None -> failwith ("new instance: under-applied typeclass"))
 	  cl
-      | Explicit -> cl
+      | Explicit -> cl, Idset.empty
   in
   let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
   let k, ctx', imps, subst =
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 5633b7273..c5b54df33 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -127,7 +127,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
     ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri =
   let env = Global.env() in
   let evars = ref Evd.empty in
-  let tclass =
+  let tclass, ids =
     match bk with
     | Implicit ->
 	Implicit_quantifiers.implicit_application Idset.empty ~allow_partial:false
@@ -138,7 +138,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 		  t, avoid
 	    | None -> failwith ("new instance: under-applied typeclass"))
 	  cl
-    | Explicit -> cl
+    | Explicit -> cl, Idset.empty
   in
   let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
   let k, ctx', len, imps, subst =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e02079fad..664b05f1d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -163,7 +163,7 @@ let make_cases s =
 let show_match id =
   try
     let s = string_of_id (snd id) in
-    let patterns = make_cases s in
+    let patterns = List.rev (make_cases s) in
     let cases =
       List.fold_left
 	(fun acc x ->