gistfile1.txt

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 428ddd6..d57ced6 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -233,6 +233,11 @@ let combine_params avoid fn applied needed =
       | (x, None) :: app, (None, (Name id, _, _)) :: need ->
 	  aux (x :: ids) avoid app need
 
+      | _, (Some (_,false), (Name id, _, _)) :: need ->
+	    aux (CHole (dummy_loc, None) :: ids) avoid app need
+      (*| x:: app, (Some cl, (Name id, _, _) as d) :: need when let s =
+              string_of_id id in String.length s > 1 && 'Z' = String.get s 1 ->
+	    aux (fst x:: ids) avoid app need *)
       | _, (Some cl, (_, _, _) as d) :: need ->
 	  let t', avoid' = fn avoid d in
 	    aux (t' :: ids) avoid' app need
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4abc2e5..1c3b60c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -573,7 +573,10 @@ GEXTEND Gram
 	     | IDENT "No"; IDENT "Variables" -> None
 	     | ["Variable" | IDENT "Variables"];
 		  idl = LIST1 identref -> Some idl ] ->
-	     VernacGeneralizable (use_non_locality (), gen) ] ]
+	     VernacGeneralizable (use_non_locality (), gen)
+      | IDENT "Ungereralizable"; IDENT "Arguments";
+          qid = smart_global; "["; l = LIST0 ident; "]" -> VernacUngeneralizableArguments (use_section_locality (),qid,l)
+ ] ]
   ;
   implicit_name:
     [ [ "!"; id = ident -> (id, false, true)
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 0d5f7b8..fa39aee 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -64,7 +64,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 	    match clname with
 	    | Some (cl, b) ->
 		let t =
-		  if b then
+		  if true then
 		    let _k = class_info cl in
 		      CHole (Util.dummy_loc, Some Evd.InternalHole)
 		  else CHole (Util.dummy_loc, None)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e2ed7c1..068650d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -798,6 +798,22 @@ let vernac_declare_implicits local r = function
       Impargs.declare_manual_implicits local (smart_global r) ~enriching:false
 	(List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps)
 
+open Typeclasses
+let vernac_ungeralizable_arguments local g l =
+  match class_of_constr (constr_of_global (smart_global g)) with
+  | Some tc ->
+      let (ci, rd) = tc.cl_context in
+      let pars = List.combine ci rd in
+      let newgr = List.map (function
+	| Some (gr, _), ((Name id, _, _) as d) when List.mem id l -> Some (gr, false), d
+	| x -> x) pars in
+      add_class { cl_impl = tc.cl_impl;
+		  cl_context = List.split newgr;
+		  cl_props = tc.cl_props;
+		  cl_projs = tc.cl_projs}
+  | None -> user_err_loc (dummy_loc, "declare_instance",
+			     Pp.str "Constant does not build instances of a declared type class.")
+
 let vernac_reserve bl =
   let sb_decl = (fun (idl,c) ->
     let t = Constrintern.interp_type Evd.empty (Global.env()) c in
@@ -1401,6 +1417,7 @@ let interp c = match c with
   | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
   | VernacReserve bl -> vernac_reserve bl
   | VernacGeneralizable (local,gen) -> vernac_generalizable local gen
+  | VernacUngeneralizableArguments (local,qid,l) ->vernac_ungeralizable_arguments local qid l
   | VernacSetOpacity (local,qidl) -> vernac_set_opacity local qidl
   | VernacSetOption (locality,key,v) -> vernac_set_option locality key v
   | VernacUnsetOption (locality,key) -> vernac_unset_option locality key
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 72c9b1f..2aaa443 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -305,6 +305,7 @@ type vernac_expr =
       (explicitation * bool * bool) list list
   | VernacReserve of simple_binder list
   | VernacGeneralizable of locality_flag * (lident list) option
+  | VernacUngeneralizableArguments of locality_flag * reference or_by_notation * identifier list
   | VernacSetOpacity of
       locality_flag * (Conv_oracle.level * reference or_by_notation list) list
   | VernacUnsetOption of full_locality_flag * Goptions.option_name