Add the ability to specify the implicit status of section variables and

whether or not to keep them regardless of the actual dependencies (in
order to implement the proper discharge behavior for type classes). 
This means adding an argument to rebuild_function in libobject, giving
this information on variables after a section's constants have been
discharged (discharge_function is too early). Surface syntax for
Variable not added yet.


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

16 files changed, 113 insertions, 88 deletions

diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index e7a727bb5..ac4b9642e 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -100,7 +100,7 @@ let declare_assumption env isevars idl is_coe k bl c nl =
       Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None 
     in
     let c = solve_tccs_in_type env id isevars evm c typ in
-      List.iter (Command.declare_one_assumption is_coe k c imps nl) idl
+      List.iter (Command.declare_one_assumption is_coe k c imps false false nl) idl
   else
     errorlabstrm "Command.Assumption"
 	(str "Cannot declare an assumption while in proof editing mode.")
diff --git a/interp/notation.ml b/interp/notation.ml
index b04f3be03..f3ecbd446 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -467,7 +467,7 @@ let discharge_arguments_scope (_,(req,r,l)) =
   if req = ArgsScopeNoDischarge then None
   else Some (req,pop_global_reference r,l)
 
-let rebuild_arguments_scope (req,r,l) =
+let rebuild_arguments_scope (_,(req,r,l)) =
   match req with
     | ArgsScopeNoDischarge -> assert false
     | ArgsScopeAuto ->
diff --git a/library/declare.ml b/library/declare.ml
index da2c1b778..278acc665 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -57,7 +57,7 @@ let set_xml_declare_inductive f = xml_declare_inductive := if_xml f
 
 type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
-  | SectionLocalAssum of types
+  | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *)
 
 type variable_declaration = dir_path * section_variable_entry * logical_kind
 
@@ -84,17 +84,17 @@ let cache_variable ((sp,_),o) =
   (* Constr raisonne sur les noms courts *)
   if Idmap.mem id !vartab then
     errorlabstrm "cache_variable" (pr_id id ++ str " already exists");
-  let vd = match d with (* Fails if not well-typed *)
-    | SectionLocalAssum ty ->
+  let vd,impl,keep = match d with (* Fails if not well-typed *)
+    | SectionLocalAssum (ty, impl, keep) ->
         let cst = Global.push_named_assum (id,ty) in
         let (_,bd,ty) = Global.lookup_named id in
-        CheckedSectionLocalAssum (ty,cst)
+        CheckedSectionLocalAssum (ty,cst), impl, if keep then Some ty else None
     | SectionLocalDef (c,t,opaq) -> 
         let cst = Global.push_named_def (id,c,t) in
         let (_,bd,ty) = Global.lookup_named id in
-        CheckedSectionLocalDef (Option.get bd,ty,cst,opaq) in
+        CheckedSectionLocalDef (Option.get bd,ty,cst,opaq), false, None in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
-  add_section_variable id;
+  add_section_variable id impl keep;
   Dischargedhypsmap.set_discharged_hyps sp [];
   vartab := Idmap.add id (p,vd,mk) !vartab
 
diff --git a/library/declare.mli b/library/declare.mli
index f04170b34..96fd5eb9b 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -34,7 +34,7 @@ open Nametab
 
 type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
-  | SectionLocalAssum of types
+  | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *)
 
 type variable_declaration = dir_path * section_variable_entry * logical_kind
 
diff --git a/library/impargs.ml b/library/impargs.ml
index 9ffd103de..fc2d63ca8 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -240,12 +240,6 @@ let compute_implicits_flags env f all t =
     (f.strict or f.strongly_strict) f.strongly_strict
     f.reversible_pattern f.contextual all env t
     
-let compute_implicits_auto env f t =
-  let l = compute_implicits_flags env f false t in
-    prepare_implicits f l
-
-let compute_implicits env t = compute_implicits_auto env !implicit_args t
-
 let set_implicit id imp insmax =
   (id,(match imp with None -> Manual false | Some imp -> imp),insmax)
 
@@ -258,7 +252,7 @@ let rec assoc_by_pos k = function
   | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl
   | [] -> raise Not_found
 
-let compute_manual_implicits flags env t enriching l =
+let compute_manual_implicits env flags t enriching l =
   let autoimps =
     if enriching then compute_implicits_flags env flags true t
     else compute_implicits_gen false false false true true env t in
@@ -296,8 +290,9 @@ let compute_manual_implicits flags env t enriching l =
 	forced :: merge (k+1) l' imps
   | [] when l = [] -> []
   | [] ->
-      match List.hd l with
-	| ExplByName id,b ->
+      List.iter (function 
+	| ExplByName id,(b,forced) -> 
+	    if not forced then
 	      error ("Wrong or not dependent implicit argument name: "^(string_of_id id))
 	| ExplByPos (i,_id),_t ->
 	    if i<1 or i>n then 
@@ -305,10 +300,19 @@ let compute_manual_implicits flags env t enriching l =
 	    else
 	      errorlabstrm ""
 		(str "Cannot set implicit argument number " ++ int i ++
-		    str ": it has no name")
+		    str ": it has no name"))
+	l; []
   in
   merge 1 l autoimps
 
+let compute_implicits_auto env f manual t =
+  match manual with
+      [] -> let l = compute_implicits_flags env f false t in
+	      prepare_implicits f l
+    | _ -> compute_manual_implicits env f t true manual
+	
+let compute_implicits env t = compute_implicits_auto env !implicit_args [] t
+
 type maximal_insertion = bool (* true = maximal contextual insertion *)
 
 type implicit_status =
@@ -353,16 +357,16 @@ let positions_of_implicits =
 
 (*s Constants. *)
 
-let compute_constant_implicits flags cst =
+let compute_constant_implicits flags manual cst =
   let env = Global.env () in
-  compute_implicits_auto env flags (Typeops.type_of_constant env cst)
+  compute_implicits_auto env flags manual (Typeops.type_of_constant env cst)
 
 (*s Inductives and constructors. Their implicit arguments are stored
    in an array, indexed by the inductive number, of pairs $(i,v)$ where
    $i$ are the implicit arguments of the inductive and $v$ the array of 
    implicit arguments of the constructors. *)
 
-let compute_mib_implicits flags kn =
+let compute_mib_implicits flags manual kn =
   let env = Global.env () in
   let mib = lookup_mind kn env in
   let ar =
@@ -375,34 +379,34 @@ let compute_mib_implicits flags kn =
   let imps_one_inductive i mip =
     let ind = (kn,i) in
     let ar = type_of_inductive env (mib,mip) in
-    ((IndRef ind,compute_implicits_auto env flags ar),
+    ((IndRef ind,compute_implicits_auto env flags manual ar),
      Array.mapi (fun j c ->
-       (ConstructRef (ind,j+1),compute_implicits_auto env_ar flags c))
+       (ConstructRef (ind,j+1),compute_implicits_auto env_ar flags manual c))
        mip.mind_nf_lc)
   in
   Array.mapi imps_one_inductive mib.mind_packets
 
-let compute_all_mib_implicits flags kn =
-  let imps = compute_mib_implicits flags kn in
+let compute_all_mib_implicits flags manual kn =
+  let imps = compute_mib_implicits flags manual kn in
   List.flatten 
     (array_map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps)
 
 (*s Variables. *)
 
-let compute_var_implicits flags id =
+let compute_var_implicits flags manual id =
   let env = Global.env () in
   let (_,_,ty) = lookup_named id env in
-  compute_implicits_auto env flags ty
+  compute_implicits_auto env flags manual ty
 
 (* Implicits of a global reference. *)
 
-let compute_global_implicits flags = function
-  | VarRef id -> compute_var_implicits flags id
-  | ConstRef kn -> compute_constant_implicits flags kn
+let compute_global_implicits flags manual = function
+  | VarRef id -> compute_var_implicits flags manual id
+  | ConstRef kn -> compute_constant_implicits flags manual kn
   | IndRef (kn,i) -> 
-      let ((_,imps),_) = (compute_mib_implicits flags kn).(i) in imps
+      let ((_,imps),_) = (compute_mib_implicits flags manual kn).(i) in imps
   | ConstructRef ((kn,i),j) -> 
-      let (_,cimps) = (compute_mib_implicits flags kn).(i) in snd cimps.(j-1)
+      let (_,cimps) = (compute_mib_implicits flags manual kn).(i) in snd cimps.(j-1)
 
 (* Merge a manual explicitation with an implicit_status list *)
 
@@ -459,19 +463,23 @@ let discharge_implicits (_,(req,l)) =
   | ImplMutualInductive (kn,flags) ->
       Some (ImplMutualInductive (pop_kn kn,flags),l)
 
-let rebuild_implicits (req,l) =
+let rebuild_implicits (info,(req,l)) =
+  let manual = List.fold_left (fun acc (id, impl, keep) -> 
+    if impl then (ExplByName id, (true, true)) :: acc else acc)
+    [] info
+  in
   let l' = match req with
   | ImplNoDischarge -> assert false
   | ImplConstant (con,flags) -> 
-      [ConstRef con,compute_constant_implicits flags con]
+      [ConstRef con, compute_constant_implicits flags manual con]
   | ImplMutualInductive (kn,flags) ->
-      compute_all_mib_implicits flags kn
+      compute_all_mib_implicits flags manual kn
   | ImplInteractive (ref,flags,o) ->
       match o with
-      | ImplAuto -> [ref,compute_global_implicits flags ref]
+      | ImplAuto -> [ref,compute_global_implicits flags manual ref]
       | ImplManual l -> 
-	  let auto = compute_global_implicits flags ref in
-	  let auto = if flags.main then auto else List.map (fun _ -> None) auto in
+	  let auto = compute_global_implicits flags manual ref in
+(* 	  let auto = if flags.main then auto else List.map (fun _ -> None) auto in *)
 	  let l' = merge_impls auto l in [ref,l']
   in (req,l')
     
@@ -487,7 +495,7 @@ let (inImplicits, _) =
     export_function = (fun x -> Some x) }
 
 let declare_implicits_gen req flags ref =
-  let imps = compute_global_implicits flags ref in
+  let imps = compute_global_implicits flags [] ref in
   add_anonymous_leaf (inImplicits (req,[ref,imps]))
 
 let declare_implicits local ref =
@@ -510,7 +518,7 @@ let declare_mib_implicits kn =
     let flags = !implicit_args in
     let imps = array_map_to_list
       (fun (ind,cstrs) -> ind::(Array.to_list cstrs))
-      (compute_mib_implicits flags kn) in
+      (compute_mib_implicits flags [] kn) in
     add_anonymous_leaf
       (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
 
@@ -518,13 +526,13 @@ let declare_mib_implicits kn =
 type manual_explicitation = Topconstr.explicitation * (bool * bool) 
 
 let compute_implicits_with_manual env typ enriching l = 
-  compute_manual_implicits !implicit_args env typ enriching l
+  compute_manual_implicits env !implicit_args typ enriching l
 
 let declare_manual_implicits local ref enriching l =
   let flags = !implicit_args in
   let env = Global.env () in
   let t = Global.type_of_global ref in
-  let l' = compute_manual_implicits flags env t enriching l in
+  let l' = compute_manual_implicits env flags t enriching l in
   let req =
     if local or isVarRef ref then ImplNoDischarge
     else ImplInteractive(ref,flags,ImplManual l')
diff --git a/library/impargs.mli b/library/impargs.mli
index e7b05f422..120660027 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -59,7 +59,8 @@ val compute_implicits : env -> types -> implicits_list
    maximal insertion and forcing flags. *)
 type manual_explicitation = Topconstr.explicitation * (bool * bool)
 
-val compute_implicits_with_manual : env -> types -> bool -> manual_explicitation list -> implicits_list
+val compute_implicits_with_manual : env -> types -> bool -> 
+  manual_explicitation list -> implicits_list
 
 (*s Computation of implicits (done using the global environment). *)
 
diff --git a/library/lib.ml b/library/lib.ml
index 4acdba88c..1db433c19 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -214,9 +214,9 @@ let add_leaf id obj =
   add_entry oname (Leaf obj);
   oname
 
-let add_discharged_leaf id obj =
+let add_discharged_leaf id varinfo obj =
   let oname = make_oname id in
-  let newobj = rebuild_object obj in
+  let newobj = rebuild_object (varinfo, obj) in
   cache_object (oname,newobj);
   add_entry oname (Leaf newobj)
 
@@ -440,18 +440,19 @@ let what_is_opened () = find_entry_p is_something_opened
 type abstr_list = Sign.named_context Cmap.t * Sign.named_context KNmap.t
 
 let sectab =
-  ref ([] : (identifier list * Cooking.work_list * abstr_list) list)
+  ref ([] : ((identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list)
 
 let add_section () =
   sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab
 
-let add_section_variable id =
+let add_section_variable id impl keep =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
-    | (vars,repl,abs)::sl -> sectab := (id::vars,repl,abs)::sl
+    | (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl
 
 let rec extract_hyps = function
-  | (id::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps)
+  | ((id,impl,keep)::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps)
+  | ((id,impl,Some ty)::idl,hyps) -> (id,None,ty) :: extract_hyps (idl,hyps)
   | (id::idl,hyps) -> extract_hyps (idl,hyps)
   | [], _ -> []
 
@@ -473,6 +474,8 @@ let add_section_constant kn =
 
 let replacement_context () = pi2 (List.hd !sectab)
 
+let variables_context () = pi1 (List.hd !sectab)
+
 let section_segment_of_constant con =
   Cmap.find con (fst (pi3 (List.hd !sectab)))
 
@@ -548,6 +551,10 @@ let close_section id =
     with Not_found ->
       error "no opened section"
   in
+  let var_info = List.map
+    (fun (x, y, z) -> (x, y, match z with Some _ -> true | None -> false))
+    (variables_context ())
+  in
   let (secdecls,secopening,before) = split_lib oname in
   lib_stk := before;
   let full_olddir = fst !path_prefix in
@@ -556,7 +563,7 @@ let close_section id =
   if !Flags.xml_export then !xml_close_section id;
   let newdecls = List.map discharge_item secdecls in
   Summary.section_unfreeze_summaries fs;
-  List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
+  List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id var_info o)) newdecls;
   Cooking.clear_cooking_sharing ();
   Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
 
diff --git a/library/lib.mli b/library/lib.mli
index 6c826af63..da8ace048 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -175,7 +175,7 @@ val section_segment_of_mutual_inductive: mutual_inductive -> Sign.named_context
 
 val section_instance : global_reference -> identifier array
 
-val add_section_variable : identifier -> unit
+val add_section_variable : identifier -> bool -> Term.types option -> unit
 val add_section_constant : constant -> Sign.named_context -> unit
 val add_section_kn : kernel_name -> Sign.named_context -> unit
 val replacement_context : unit ->
diff --git a/library/libobject.ml b/library/libobject.ml
index 7c74d402b..b24a46e38 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -28,6 +28,7 @@ let relax b = relax_flag := b;;
 type 'a substitutivity = 
     Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
 
+type discharge_info = (identifier * bool * bool) list
 
 type 'a object_declaration = {
   object_name : string;
@@ -37,7 +38,7 @@ type 'a object_declaration = {
   classify_function : object_name * 'a -> 'a substitutivity;
   subst_function : object_name * substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
-  rebuild_function : 'a -> 'a;
+  rebuild_function : discharge_info * 'a -> 'a;
   export_function : 'a -> 'a option }
 
 let yell s = anomaly s
@@ -51,7 +52,7 @@ let default_object s = {
     yell ("The object "^s^" does not know how to substitute!"));
   classify_function = (fun (_,obj) -> Keep obj);
   discharge_function = (fun _ -> None);
-  rebuild_function = (fun x -> x);
+  rebuild_function = (fun (_,x) -> x);
   export_function = (fun _ -> None)} 
 
 
@@ -77,7 +78,7 @@ type dynamic_object_declaration = {
   dyn_subst_function : object_name * substitution * obj -> obj;
   dyn_classify_function : object_name * obj -> obj substitutivity;
   dyn_discharge_function : object_name * obj -> obj option;
-  dyn_rebuild_function : obj -> obj;
+  dyn_rebuild_function : discharge_info * obj -> obj;
   dyn_export_function : obj -> obj option }
 
 let object_tag lobj = Dyn.tag lobj
@@ -115,8 +116,8 @@ let declare_object odecl =
       Option.map infun (odecl.discharge_function (oname,outfun lobj))
     else 
       anomaly "somehow we got the wrong dynamic object in the dischargefun"
-  and rebuild lobj = 
-    if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj))
+  and rebuild (varinfo,lobj) = 
+    if Dyn.tag lobj = na then infun (odecl.rebuild_function (varinfo,outfun lobj))
     else anomaly "somehow we got the wrong dynamic object in the rebuildfun"
   and exporter lobj = 
     if Dyn.tag lobj = na then 
@@ -173,8 +174,8 @@ let classify_object ((_,lobj) as node) =
 let discharge_object ((_,lobj) as node) = 
   apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj
 
-let rebuild_object lobj =
-  apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj
+let rebuild_object ((_,lobj) as node) =
+  apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function node) lobj
 
 let export_object lobj =
   apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index 540b69feb..15de388ea 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -63,6 +63,8 @@ open Mod_subst
 type 'a substitutivity = 
     Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
 
+type discharge_info = (identifier * bool * bool) list
+
 type 'a object_declaration = {
   object_name : string;
   cache_function : object_name * 'a -> unit;
@@ -71,7 +73,7 @@ type 'a object_declaration = {
   classify_function : object_name * 'a -> 'a substitutivity;
   subst_function : object_name * substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
-  rebuild_function : 'a -> 'a;
+  rebuild_function : discharge_info * 'a -> 'a;
   export_function : 'a -> 'a option }
 
 (* The default object is a "Keep" object with empty methods. 
@@ -106,5 +108,5 @@ val subst_object : object_name * substitution * obj -> obj
 val classify_object : object_name * obj -> obj substitutivity
 val export_object : obj -> obj option
 val discharge_object : object_name * obj -> obj option
-val rebuild_object : obj -> obj
+val rebuild_object : discharge_info * obj -> obj
 val relax : bool -> unit
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 4c944f460..191343a55 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -90,8 +90,8 @@ let gmap_list_merge old upd ne =
       let oldv = try Gmap.find k old with Not_found -> [] in
       let v' = 
 	List.fold_left (fun acc x -> 
-	  if not (List.exists (fun y -> y.is_impl = x.is_impl) v) then
-	    (x :: acc) else acc)
+	  if not (List.exists (fun y -> y.is_impl = x.is_impl) v) then (
+	    (x :: acc)) else acc)
 	v oldv
       in Gmap.add k v' acc)
       ne Gmap.empty
@@ -106,17 +106,15 @@ let gmap_list_merge old upd ne =
       old ne
 
 let add_instance_hint_ref = ref (fun id pri -> assert false)
-let register_add_instance_hint = (:=) add_instance_hint_ref
+let register_add_instance_hint =
+  (:=) add_instance_hint_ref
 let add_instance_hint id = !add_instance_hint_ref id
 
-let qualid_of_con c = 
-  Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c))
-
 let cache (_, (cl, m, inst)) =
   classes := gmap_merge !classes cl;
   methods := gmap_merge !methods m;
-  instances := gmap_list_merge !instances 
-    (fun i -> add_instance_hint (qualid_of_con i.is_impl))
+  instances := gmap_list_merge !instances
+    (fun (i : instance) -> add_instance_hint i.is_impl i.is_pri)
     inst
 
 open Libobject
@@ -179,11 +177,17 @@ let discharge (_,(cl,m,inst)) =
       { is_impl = Lib.discharge_con is.is_impl;
 	is_pri = is.is_pri;
 	is_class = Gmap.find (Lib.discharge_global is.is_class.cl_impl) classes; })
-      insts
+      insts;
   in
   let instances = Gmap.map subst_inst inst in
     Some (classes, m, instances)
   
+let rebuild (_,(cl,m,inst as obj)) =
+  Gmap.iter (fun _ insts -> 
+    List.iter (fun is -> add_instance_hint is.is_impl is.is_pri) insts) 
+    inst;
+  obj
+
 let (input,output) = 
   declare_object
     { (default_object "type classes state") with
@@ -192,6 +196,7 @@ let (input,output) =
       open_function = (fun _ -> cache);
       classify_function = (fun (_,x) -> Substitute x);
       discharge_function = discharge;
+(*       rebuild_function = rebuild; *)
       subst_function = subst;
       export_function = (fun x -> Some x) }
 
@@ -228,7 +233,7 @@ let instances_of c =
 let add_instance i =
   let cl = Gmap.find i.is_class.cl_impl !classes in
     instances := gmapl_add cl.cl_impl { i with is_class = cl } !instances;
-    add_instance_hint (qualid_of_con i.is_impl) i.is_pri;
+    add_instance_hint i.is_impl i.is_pri;
     update ()
 
 let instances r = 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 2646c09dd..c091842f0 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -52,8 +52,8 @@ val typeclasses : unit -> typeclass list
 val add_class : typeclass -> unit
 val add_instance : instance -> unit
 
-val register_add_instance_hint : (reference -> int option -> unit) -> unit
-val add_instance_hint : reference -> int option -> unit
+val register_add_instance_hint : (constant -> int option -> unit) -> unit
+val add_instance_hint : constant -> int option -> unit
 
 val class_info : global_reference -> typeclass (* raises a UserError if not a class *)
 val is_class : global_reference -> bool
@@ -89,9 +89,6 @@ val nf_substitution : evar_map -> substitution -> substitution
 
 val is_implicit_arg : hole_kind -> bool
 
-val qualid_of_con : Names.constant -> Libnames.reference
-
-
 (* debug *)
 
 (* val subst :  *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 535dda623..bc627a283 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -33,11 +33,14 @@ open Entries
 
 let hint_db = "typeclass_instances"
 
+let qualid_of_con c = 
+  Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c))
+
 let _ =
   Typeclasses.register_add_instance_hint 
     (fun inst pri ->
       Auto.add_hints false [hint_db] 
-	(Vernacexpr.HintsResolve [pri, CAppExpl (dummy_loc, (None, inst), [])]))
+	(Vernacexpr.HintsResolve [pri, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])]))
 
 let declare_instance_constant con =
   let instance = Typeops.type_of_constant (Global.env ()) con in
@@ -593,7 +596,7 @@ let context ?(hook=fun _ -> ()) l =
 	    | None -> ()
       else
 	(Command.declare_one_assumption false (Local (* global *), Definitional) t
-	    [] false (* inline *) (dummy_loc, id);
+	    [] true (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id);
 	 match class_of_constr t with
 	     None -> ()
 	   | Some tc -> hook (VarRef id)))
diff --git a/toplevel/command.ml b/toplevel/command.ml
index fbba7a4ee..bc8f6c9ee 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -172,12 +172,12 @@ let syntax_definition ident (vars,c) local onlyparse =
 let assumption_message id =
   if_verbose message ((string_of_id id) ^ " is assumed")
 
-let declare_one_assumption is_coe (local,kind) c imps nl (_,ident) =
+let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) =
   let r = match local with
     | Local when Lib.sections_are_opened () ->
         let _ = 
           declare_variable ident 
-            (Lib.cwd(), SectionLocalAssum c, IsAssumption kind) in
+            (Lib.cwd(), SectionLocalAssum (c,impl,keep), IsAssumption kind) in
         assumption_message ident;
         if is_verbose () & Pfedit.refining () then 
           msgerrnl (str"Warning: Variable " ++ pr_id ident ++ 
@@ -198,13 +198,13 @@ let declare_one_assumption is_coe (local,kind) c imps nl (_,ident) =
 let declare_assumption_hook = ref ignore
 let set_declare_assumption_hook = (:=) declare_assumption_hook
 
-let declare_assumption idl is_coe k bl c nl=
+let declare_assumption idl is_coe k bl c impl keep nl =
   if not (Pfedit.refining ()) then 
     let c = generalize_constr_expr c bl in
     let env = Global.env () in
     let c', imps = interp_type_evars_impls env c in
       !declare_assumption_hook c';
-      List.iter (declare_one_assumption is_coe k c' imps nl) idl
+      List.iter (declare_one_assumption is_coe k c' imps impl keep nl) idl
   else
     errorlabstrm "Command.Assumption"
 	(str "Cannot declare an assumption while in proof editing mode.")
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 942fd2c31..8a987ef6c 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -43,13 +43,14 @@ val syntax_definition : identifier -> identifier list * constr_expr ->
   bool -> bool -> unit
 
 val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types ->
-  Impargs.manual_explicitation list -> bool -> Names.variable located  -> unit
-
+  Impargs.manual_explicitation list ->
+  bool (* implicit *) -> bool (* keep *) -> bool (* inline *) -> Names.variable located  -> unit
+  
 val set_declare_assumption_hook : (types -> unit) -> unit
 
 val declare_assumption : identifier located list ->
-  coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> bool 
-  ->unit
+  coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> 
+  bool -> bool -> bool -> unit
 
 val declare_interning_data : 'a * Constrintern.implicits_env ->
     string * Topconstr.constr_expr * Topconstr.scope_name option -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1ea732add..f5768888c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -353,7 +353,7 @@ let vernac_exact_proof c =
 	(str "Command 'Proof ...' can only be used at the beginning of the proof")
   	
 let vernac_assumption kind l nl=
-  List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c nl) l
+  List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c false false nl) l
 
 let vernac_inductive f indl = build_mutual indl f