Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from

svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses

........
  r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line
  
  Comment grammar error
........
  r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines
  
  The initial Type Classes patch.
  This patch introduces type classes and instance definitions a la Haskell.
  Technically, it uses the implicit arguments mechanism which was extended a bit. 
  The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters.
  It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). 
........
  r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line
  
  Fix interface
........
  r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line
  
  Fix more xlate code
........
  r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines
  
  Update coqdoc for type classes, fix proof state not being displayed on Next Obligation.
........
  r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines
  
  Bug fixes in Instance decls.
........
  r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines
  
  Streamline typeclass context implementation, prepare for class binders in proof statements.
........
  r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line
  
  Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions
........
  r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines
  
  Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context.
........
  r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line
  
  Stupid bug
........
  r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line
  
  Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints
........
  r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line
  
  Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors
........
  r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines
  
  Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent.
  New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental.
  Other bugs related to naming in typeclasses fixed. 
........
  r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines
  
  Progress on setoids using type classes, recognize setoid equalities in hyps better.
  Streamline implementation to return more information when resolving setoids (return the results setoid).
........
  r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line
  
  Syntax change, more like Coq
........
  r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line
  
  Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax
........
  r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines
  
  Work on type classes based rewrite tactic.
........
  r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines
  
  Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets.
........
  r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line
  
  Forgot to add a file
........
  r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines
  
  Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and 
  implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts.
........
  r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines
  
  Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. 
  Add useful tactics to Program.Subsets.
........


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

13 files changed, 733 insertions, 34 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 5a1b8b8b4a..bad30a8491 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -77,6 +77,8 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
       hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx te)
   | PretypeError(ctx,te) ->
       hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te)
+  | Typeclasses_errors.TypeClassError(env, te) ->
+      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_typeclass_error env te)
   | InductiveError e -> 
       hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e)
   | RecursionSchemeError e -> 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
new file mode 100644
index 0000000000..7ee4513d1f
--- /dev/null
+++ b/toplevel/classes.ml
@@ -0,0 +1,505 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*)
+
+(*i*)
+open Names
+open Decl_kinds
+open Term
+open Termops
+open Sign
+open Entries
+open Evd
+open Environ
+open Nametab
+open Mod_subst
+open Util
+open Typeclasses_errors
+open Typeclasses
+open Libnames
+open Constrintern
+open Rawterm
+open Topconstr
+(*i*)
+
+let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
+(* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *)
+let mismatched_props env n m = mismatched_ctx_inst env Properties n m
+
+type binder_list = (identifier located * constr_expr) list
+
+let interp_binders_evars isevars env avoid l =
+  List.fold_left
+    (fun (env, ids, params) ((loc, i), t) -> 
+      let n = Name i in
+      let t' = interp_binder_evars isevars env n t in
+      let d = (i,None,t') in
+	(push_named d env, i :: ids, d::params))
+    (env, avoid, []) l
+
+let interp_typeclass_context_evars isevars env avoid l =
+  List.fold_left
+    (fun (env, ids, params) (iid, bk, l) -> 
+      let t' = interp_binder_evars isevars env (snd iid) l in
+      let i = match snd iid with
+	| Anonymous -> Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids
+	| Name id -> id
+      in
+      let d = (i,None,t') in
+	(push_named d env, i :: ids, d::params))
+    (env, avoid, []) l
+
+let interp_constrs_evars isevars env avoid l =
+  List.fold_left
+    (fun (env, ids, params) t -> 
+      let t' = interp_binder_evars isevars env Anonymous t in
+      let id = Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids in
+      let d = (id,None,t') in
+	(push_named d env, id :: ids, d::params))
+    (env, avoid, []) l
+
+let raw_assum_of_binders k = 
+  List.map (fun ((loc,i),t) -> LocalRawAssum ([(loc, Name i)], k, t))
+
+let raw_assum_of_constrs k = 
+  List.map2 (fun t (n,_,_) -> LocalRawAssum ([(dummy_loc, Name n)], k, t))
+
+let raw_assum_of_anonymous_constrs k = 
+  List.map (fun t -> LocalRawAssum ([(dummy_loc, Anonymous)], k, t))
+
+let decl_expr_of_binders = 
+  List.map (fun ((loc,i),t) -> false, Vernacexpr.AssumExpr ((loc, Name i), t))
+      
+let rec unfold n f acc = 
+  match n with 
+    | 0 -> f 0 acc
+    | n -> unfold (n - 1) f (f n acc)
+
+(* Declare everything in the parameters as implicit, and the class instance as well *)
+open Topconstr
+
+let declare_implicit_proj c proj =
+  let len = List.length c.cl_context + List.length c.cl_super + List.length c.cl_params in
+  let (ctx, _) = decompose_prod_n (len + 1) (Typeops.type_of_constant (Global.env()) proj) in
+  let expls =
+    let rec aux i expls = function
+	[] -> expls
+      | (Name n, _) :: tl -> 
+	  let impl = ExplByPos (i, Some n), (true, true) in
+	    aux (succ i) (impl :: List.remove_assoc (ExplByName n) expls) tl
+      | (Anonymous,_) :: _ -> assert(false)
+    in
+      aux 1 [] ctx
+  in Impargs.declare_manual_implicits true (ConstRef proj) true expls
+      
+let declare_implicits cl =
+  let projs = Recordops.lookup_projections cl.cl_impl in
+    List.iter
+      (fun c -> 
+	match c with 
+	  | None -> assert(false)
+	  | Some p -> declare_implicit_proj cl p)
+      projs;
+    let indimps = 
+      list_map_i 
+	(fun i (na, b, t) -> ExplByPos (i, Some na), (false, true))
+	1 (List.rev cl.cl_context)
+    in
+      Impargs.declare_manual_implicits true (IndRef cl.cl_impl) false indimps
+
+let rel_of_named_context subst l = 
+  List.fold_right
+    (fun (id, _, t) (ctx, acc) -> (Name id, None, subst_vars acc t) :: ctx, id :: acc)
+    l ([], subst)
+
+let degenerate_decl (na,b,t) =
+  let id = match na with
+    | Name id -> id
+    | Anonymous -> anomaly "Unnamed record variable" in 
+  match b with
+    | None -> (id, Entries.LocalAssum t)
+    | Some b -> (id, Entries.LocalDef b)
+
+
+let declare_structure env id idbuild params arity fields =
+  let nparams = List.length params and nfields = List.length fields in
+  let args = extended_rel_list nfields params in
+  let ind = applist (mkRel (1+nparams+nfields), args) in
+  let type_constructor = it_mkProd_or_LetIn ind fields in
+  let mie_ind =
+    { mind_entry_typename = id;
+      mind_entry_arity = arity;
+      mind_entry_consnames = [idbuild];
+      mind_entry_lc = [type_constructor] } in
+  let mie =
+    { mind_entry_params = List.map degenerate_decl params;
+      mind_entry_record = true;
+      mind_entry_finite = true;
+      mind_entry_inds = [mie_ind] } in
+  let kn = Command.declare_mutual_with_eliminations true mie in
+  let rsp = (kn,0) in (* This is ind path of idstruc *)
+  let kinds,sp_projs = Record.declare_projections rsp (List.map (fun _ -> false) fields) fields in
+  let _build = ConstructRef (rsp,1) in
+    Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
+    rsp
+
+
+let mk_interning_data env na typ =
+  let impl =
+    if Impargs.is_implicit_args() then
+      Impargs.compute_implicits env typ
+    else []
+  in (na, ([], impl, Notation.compute_arguments_scope typ))
+    
+let interp_fields_evars isevars env avoid l =
+  List.fold_left
+    (fun (env, ids, params, impls) ((loc, i), t) -> 
+      let t' = interp_type_evars isevars env ~impls t in
+      let data = mk_interning_data env i t' in
+      let d = (i,None,t') in
+	(push_named d env, i :: ids, d::params, ([], data :: snd impls)))
+    (env, avoid, [], ([], [])) l    
+
+let new_class id par ar sup props =
+  let env0 = Global.env() in
+  let isevars = ref (Evd.create_evar_defs Evd.empty) in
+  let avoid = Termops.ids_of_context env0 in
+
+  let env_params, avoid = env0, avoid in
+
+  (* Find the implicitly quantified variables *)
+  let gen_ctx, super = Implicit_quantifiers.resolve_class_binders (vars_of_env env0) sup in
+
+  let env_super_ctx, avoid, ctx_super_ctx = interp_binders_evars isevars env_params avoid gen_ctx in
+    
+  (* Interpret the superclasses constraints *)
+  let env_super, avoid, ctx_super0 = 
+    interp_typeclass_context_evars isevars env_super_ctx avoid super 
+  in
+
+  let env_params, avoid, ctx_params = interp_binders_evars isevars env_super avoid par in
+
+  (* Interpret the arity *)
+  let arity = interp_type_evars isevars env_params (CSort (fst ar, snd ar)) in
+    
+  (* let fullarity = it_mkProd_or_LetIn (it_mkProd_or_LetIn arity ctx_defs) ctx_params in*)
+
+  (* Interpret the definitions and propositions *)
+  let env_props, avoid, ctx_props, _ = 
+    interp_fields_evars isevars env_params avoid props 
+  in
+    
+  (* Instantiate evars and check all are resolved *)
+  let isevars,_ = Evarconv.consider_remaining_unif_problems env_props !isevars in
+  let sigma = Evd.evars_of isevars in
+  let ctx_super_ctx = Implicit_quantifiers.nf_named_context sigma ctx_super_ctx in
+  let ctx_super = Implicit_quantifiers.nf_named_context sigma ctx_super0 in
+  let ctx_params = Implicit_quantifiers.nf_named_context sigma ctx_params in
+  let ctx_props = Implicit_quantifiers.nf_named_context sigma ctx_props in
+  let arity = Reductionops.nf_evar sigma arity in
+  let ce t = Evarutil.check_evars env0 Evd.empty isevars t in
+  let kn = 
+    let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
+    let params, subst = rel_of_named_context [] (ctx_params @ ctx_super @ ctx_super_ctx) in
+    let fields, _ = rel_of_named_context subst ctx_props in
+      List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields);
+      declare_structure env0 (snd id) idb params arity fields
+  in
+  let ctx_context, ctx_super = 
+    let class_binders, regular_binders = 
+      List.partition (fun (na, b, t) -> 
+	Typeclasses.class_of_constr t <> None)
+	ctx_super_ctx
+    in 
+      if (ctx_super_ctx = class_binders @ regular_binders) then
+	regular_binders, ctx_super @ class_binders
+      else ctx_super_ctx, ctx_super
+  in
+  let k =
+    { cl_name = snd id;
+      cl_context = ctx_context;
+      cl_super = ctx_super;
+      cl_params = ctx_params;
+      cl_props = ctx_props;
+      cl_impl = kn }
+  in
+    declare_implicits k;
+    add_class k
+    
+open Decl_kinds
+open Entries
+
+let hint_db = "typeclass_instances"
+
+let add_instance_hint inst = 
+  Auto.add_hints false [hint_db] (Vernacexpr.HintsResolve [CRef (Ident (dummy_loc, inst))])
+
+let declare_instance (_,id) =
+  add_instance_hint id
+
+type binder_def_list = (identifier located * identifier located list * constr_expr) list
+
+let binders_of_lidents l =
+  List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Implicit, CHole loc)) l
+
+let subst_ids_in_named_context subst l =
+  let x, _ = 
+    List.fold_right
+      (fun (id, _, t) (ctx, k) -> (id, None, substn_vars k subst t) :: ctx, succ k)
+      l ([], 1)
+  in x
+    
+let subst_one_named inst ids t =
+  substnl inst 0 (substn_vars 1 ids t)
+      
+let subst_named inst subst ctx =
+  let ids = List.map (fun (id, _, _) -> id) subst in
+  let ctx' = subst_ids_in_named_context ids ctx in
+  let ctx', _ =
+    List.fold_right
+      (fun (id, _, t) (ctx, k) -> (id, None, substnl inst k t) :: ctx, succ k)
+      ctx' ([], 0)
+  in ctx'
+
+let push_named_context = List.fold_right push_named
+
+let destClass c = 
+  match kind_of_term c with
+      App (c, args) -> 
+	(match kind_of_term c with
+	  | Ind ind -> (try class_of_inductive ind, args with _ -> assert false)
+	  | _ -> assert false)
+    | _ -> assert false
+
+let infer_super_instances env params params_ctx super =
+  let super = subst_named params params_ctx super in
+    List.fold_right 
+      (fun (na, _, t) (sups, ids, supctx) -> 
+	let t = subst_one_named sups ids t in
+	let inst = 
+	  try resolve_one_typeclass env t 
+	  with Not_found -> 
+	    let cl, args = destClass t in
+	      no_instance (push_named_context supctx env) (dummy_loc, cl.cl_name) (Array.to_list args)
+	in
+	let d = (na, Some inst, t) in
+	  inst :: sups, na :: ids, d :: supctx)
+      super ([], [], [])
+      
+(* let evars_of_context ctx id n env = *)
+(*   List.fold_right (fun (na, _, t) (n, env, nc) ->  *)
+(*     let b = Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (Ident id, (n * Some na))) t in *)
+(*     let d = (na, Some b, t) in *)
+(*       (succ n, push_named d env, d :: nc)) *)
+(*     ctx (n, env, []) *)
+
+let type_ctx_instance isevars env ctx inst subst =
+  List.fold_left2
+    (fun (subst, instctx) (na, _, t) ce ->
+      let t' = replace_vars subst t in
+      let c = interp_casted_constr_evars isevars env ce t' in
+      let d = na, Some c, t' in
+	(na, c) :: subst, d :: instctx)
+    (subst, []) (List.rev ctx) inst
+
+let substitution_of_constrs ctx cstrs =
+  List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx []
+
+let destClassApp cl =
+  match cl with
+    | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l
+    | _ -> raise Not_found
+
+let new_instance sup (instid, bk, cl) props =
+  let id, par = destClassApp cl in
+  let env = Global.env() in
+  let isevars = ref (Evd.create_evar_defs Evd.empty) in
+  let avoid = Termops.ids_of_context env in
+  let k = 
+    try class_info (snd id)
+    with Not_found -> unbound_class env id
+  in
+  let gen_ctx, sup = Implicit_quantifiers.resolve_class_binders (vars_of_env env) sup in
+  let env', avoid, genctx = interp_binders_evars isevars env avoid gen_ctx in
+  let env', avoid, supctx = interp_typeclass_context_evars isevars env' avoid sup in
+  let subst = 
+    match bk with
+	Explicit ->
+	  if List.length par <> List.length k.cl_context + List.length k.cl_params then 
+	    mismatched_params env par (k.cl_params @ k.cl_context);
+	  let len = List.length k.cl_context in
+	  let ctx, par = Util.list_chop len par in
+	  let subst, _ = type_ctx_instance isevars env' k.cl_context ctx [] in
+	  let subst = 
+	    Typeclasses.substitution_of_named_context isevars env' k.cl_name len subst 
+	      k.cl_super 
+	  in 
+	    if List.length par <> List.length k.cl_params then 
+	      mismatched_params env par k.cl_params;
+	    let subst, par = type_ctx_instance isevars env' k.cl_params par subst in subst
+
+      | Implicit ->
+	  let t' = interp_type_evars isevars env (Topconstr.mkAppC (CRef (Ident id), par)) in
+	    match kind_of_term t' with 
+		App (c, args) -> 
+		  substitution_of_constrs (k.cl_params @ k.cl_super @ k.cl_context) 
+		    (List.rev (Array.to_list args))
+	      | _ -> assert false
+  in
+  isevars := Evarutil.nf_evar_defs !isevars;
+  let sigma = Evd.evars_of !isevars in
+  let env' = Implicit_quantifiers.nf_env sigma env' in
+  let subst = Typeclasses.nf_substitution sigma subst in 
+  let subst, propsctx = 
+    let props = 
+      List.map (fun (x, l, d) -> 
+	Topconstr.abstract_constr_expr d (binders_of_lidents l))
+	props
+    in
+      if List.length props <> List.length k.cl_props then 
+	mismatched_props env' props k.cl_props;
+      type_ctx_instance isevars env' k.cl_props props subst
+  in
+  let app = 
+    applistc (mkConstruct (k.cl_impl, 1)) (List.rev_map snd subst)
+  in 
+  let term = Termops.it_mkNamedLambda_or_LetIn (Termops.it_mkNamedLambda_or_LetIn app supctx) genctx in
+  isevars := Evarutil.nf_evar_defs !isevars;
+  let term = Evarutil.nf_isevar !isevars term in
+  let cdecl = 
+    let kind = IsDefinition Instance in
+    let entry = 
+      { const_entry_body   = term;
+	const_entry_type   = None;
+	const_entry_opaque = false;
+	const_entry_boxed  = false }
+    in DefinitionEntry entry, kind
+  in
+  let id, cst =
+    let instid = 
+      match snd instid with
+	  Name id -> id
+	| Anonymous -> 
+	    let i = Nameops.add_suffix (snd id) "_instance_" in
+	      Termops.next_global_ident_away false i (Termops.ids_of_context env)
+    in
+      instid, Declare.declare_constant instid cdecl
+  in 
+  let inst = 
+    { is_class = k;
+      is_name = id;
+(*       is_params = paramsctx; (\* missing gen_ctx *\) *)
+(*       is_super = superctx; *)
+      is_impl = cst;
+(*       is_add_hint = (fun () -> add_instance_hint id); *)
+    }
+  in
+    add_instance_hint id;
+    add_instance inst
+     
+let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
+
+let solve_by_tac env evd evar evi t =
+  let goal = {it = evi; sigma = (Evd.evars_of evd) } in
+  let (res, valid) = t goal in 
+    if res.it = [] then 
+      let prooftree = valid [] in
+      let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in
+	if obls = [] then 
+	  let evd' = evars_reset_evd res.sigma evd in
+	  let evd' = evar_define evar proofterm evd' in
+	    evd', true
+	else evd, false
+    else evd, false
+
+let context l =
+  let env = Global.env() in
+  let isevars = ref (Evd.create_evar_defs Evd.empty) in
+  let avoid = Termops.ids_of_context env in
+  let ctx, l = Implicit_quantifiers.resolve_class_binders (vars_of_env env) l in
+  let env', avoid, ctx = interp_binders_evars isevars env avoid ctx in
+  let env', avoid, l = interp_typeclass_context_evars isevars env' avoid l in
+  isevars := Evarutil.nf_evar_defs !isevars;
+  let sigma = Evd.evars_of !isevars in
+  let fullctx = Implicit_quantifiers.nf_named_context sigma (l @ ctx) in
+    List.iter (function (id,_,t) -> 
+      Command.declare_one_assumption false (Local (* global *), Definitional) t false (* inline *) (dummy_loc, id))
+      (List.rev fullctx)
+
+(* let init     () = hints := [] *)
+(* let freeze   () = !hints *)
+(* let unfreeze fs = hints := fs *)
+
+(* let _ = Summary.declare_summary "hints db" *)
+(* 	  { Summary.freeze_function   = freeze; *)
+(* 	    Summary.unfreeze_function = unfreeze; *)
+(* 	    Summary.init_function     = init; *)
+(* 	    Summary.survive_module = false; *)
+(* 	    Summary.survive_section   = true } *)
+
+open Libobject
+
+(* let cache (_, db) := hints := db *)
+
+(* let (input,output) =  *)
+(*   declare_object *)
+(*     { (default_object "hints db") with *)
+(*       cache_function = cache; *)
+(*       load_function = (fun _ -> cache); *)
+(*       open_function = (fun _ -> cache); *)
+(*       classify_function = (fun (_,x) -> Keep x); *)
+(*       export_function = (fun x -> Some x) } *)
+
+let tactic = ref Tacticals.tclIDTAC
+let tactic_expr = ref (Obj.magic ())
+
+let set_instantiation_tactic t = 
+  tactic := Tacinterp.interp t; tactic_expr := t
+
+let freeze () = !tactic_expr
+let unfreeze t = set_instantiation_tactic t
+let init () =  
+  set_instantiation_tactic (Tacexpr.TacId[]) 
+
+let cache (_, tac) =
+  set_instantiation_tactic tac
+
+let _ = 
+  Summary.declare_summary "typeclasses instantiation tactic"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
+      Summary.survive_module = true;
+      Summary.survive_section = true }
+
+let (input,output) = 
+  declare_object
+    { (default_object "type classes instantiation tactic state") with
+      cache_function = cache;
+      load_function = (fun _ -> cache);
+      open_function = (fun _ -> cache);
+      classify_function = (fun (_,x) -> Keep x);
+      export_function = (fun x -> Some x) }
+
+let set_instantiation_tactic t = 
+  Lib.add_anonymous_leaf (input t)
+  
+
+let initialize () =
+  if !tactic_expr = Tacexpr.TacId [] then
+    let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string "Coq.Classes.Init")) in
+      Library.require_library [qualid] None
+    
+let _ =
+  Typeclasses.solve_instanciation_problem :=
+    (fun env -> initialize ();
+      fun evd ev evi -> 
+	solve_by_tac env evd ev evi !tactic)
+      
+    
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
new file mode 100644
index 0000000000..102f1b8b04
--- /dev/null
+++ b/toplevel/classes.mli
@@ -0,0 +1,65 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
+
+(*i*)
+open Names
+open Decl_kinds
+open Term
+open Sign
+open Evd
+open Environ
+open Nametab
+open Mod_subst
+open Topconstr
+open Util
+open Typeclasses
+open Implicit_quantifiers
+(*i*)
+
+type binder_list = (identifier located * constr_expr) list
+type binder_def_list = (identifier located * identifier located list * constr_expr) list
+ 
+val binders_of_lidents : identifier located list -> local_binder list
+
+val declare_implicit_proj : typeclass -> constant -> unit
+
+val infer_super_instances : env -> constr list ->
+  named_context -> named_context -> types list * identifier list * named_context
+
+val new_class : identifier located ->
+  binder_list ->
+  Vernacexpr.sort_expr located ->
+  typeclass_context ->
+  binder_list -> unit
+
+val new_instance : 
+  typeclass_context ->
+  typeclass_constraint ->
+  binder_def_list ->
+  unit
+
+val context : typeclass_context -> unit
+
+val add_instance_hint : identifier -> unit
+
+val declare_instance : identifier located -> unit
+
+val set_instantiation_tactic : Tacexpr.raw_tactic_expr -> unit
+
+val mismatched_params : env -> constr_expr list -> named_context -> 'a
+
+val mismatched_props : env -> constr_expr list -> named_context -> 'a
+
+val solve_by_tac :     env ->
+    Evd.evar_defs ->
+    Evd.evar ->
+  evar_info ->
+  Proof_type.tactic ->
+    Evd.evar_defs * bool
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 05ee50daf5..445555251e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -46,21 +46,21 @@ open Goptions
 open Mod_subst
 open Evd
 
-let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
-let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
+let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,default_binder_kind,a,b))
+let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,default_binder_kind,a,b))
 
 let rec abstract_constr_expr c = function
   | [] -> c
   | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
-  | LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
+  | LocalRawAssum (idl,k,t)::bl ->
+      List.fold_right (fun x b -> mkLambdaC([x],k,t,b)) idl
         (abstract_constr_expr c bl)
 
 let rec generalize_constr_expr c = function
   | [] -> c
   | LocalRawDef (x,b)::bl -> mkLetInC(x,b,generalize_constr_expr c bl)
-  | LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> mkProdC([x],t,b)) idl
+  | LocalRawAssum (idl,k,t)::bl ->
+      List.fold_right (fun x b -> mkProdC([x],k,t,b)) idl
         (generalize_constr_expr c bl)
 
 let rec under_binders env f n c =
@@ -103,10 +103,13 @@ let definition_message id =
 let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
   let sigma = Evd.empty in
   let env = Global.env() in
-  match comtypopt with
+    match comtypopt with
       None -> 
 	let b = abstract_constr_expr com bl in
-	let j = interp_constr_judgment sigma env b in
+	let ib = intern_constr sigma env b in
+	let imps = Implicit_quantifiers.implicits_of_rawterm ib in
+  	let j = Default.understand_judgment sigma env ib in
+	  imps,
 	{ const_entry_body = j.uj_val;
 	  const_entry_type = None;
           const_entry_opaque = opacity;
@@ -115,7 +118,10 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
 	(* We use a cast to avoid troubles with evars in comtyp *)
 	(* that can only be resolved knowing com *)
 	let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv (DEFAULTcast,comtyp))) bl in
-	let (body,typ) = destSubCast (interp_constr sigma env b) in
+	let ib = intern_gen false sigma env b in
+	let imps = Implicit_quantifiers.implicits_of_rawterm ib in
+	let (body,typ) = destSubCast (Default.understand_gen (OfType None) sigma env ib) in
+	  imps,
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;
           const_entry_opaque = opacity;
@@ -130,15 +136,18 @@ let red_constant_entry bl ce = function
 	  (local_binders_length bl)
 	  body }
 
-let declare_global_definition ident ce local =
+let declare_global_definition ident ce local imps =
   let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in
-  if local = Local && Flags.is_verbose() then
-    msg_warning (pr_id ident ++ str" is declared as a global definition");
-  definition_message ident;
-  ConstRef kn
+  let gr = ConstRef kn in
+    if Impargs.is_implicit_args () || imps <> [] then
+      declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+    if local = Local && Flags.is_verbose() then
+      msg_warning (pr_id ident ++ str" is declared as a global definition");
+    definition_message ident;
+    gr
 
 let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
-  let ce = constant_entry_of_com (bl,c,typopt,false,boxed) in
+  let imps, ce = constant_entry_of_com (bl,c,typopt,false,boxed) in
   let ce' = red_constant_entry bl ce red_option in
   let r = match local with
     | Local when Lib.sections_are_opened () ->
@@ -152,7 +161,7 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
              str" is not visible from current goals");
         VarRef ident
     | (Global|Local) ->
-        declare_global_definition ident ce' local in
+        declare_global_definition ident ce' local imps in
   hook local r
 
 let syntax_definition ident c local onlyparse =
@@ -550,8 +559,8 @@ let eq_constr_expr c1 c2 =
 
 (* Very syntactical equality *)
 let eq_local_binder d1 d2 = match d1,d2 with
-  | LocalRawAssum (nal1,c1), LocalRawAssum (nal2,c2) ->
-      List.length nal1 = List.length nal2 &&
+  | LocalRawAssum (nal1,k1,c1), LocalRawAssum (nal2,k2,c2) ->
+      List.length nal1 = List.length nal2 && k1 = k2 &&
       List.for_all2 (fun (_,na1) (_,na2) -> na1 = na2) nal1 nal2 &&
       eq_constr_expr c1 c2
   | LocalRawDef ((_,id1),c1), LocalRawDef ((_,id2),c2) ->
@@ -742,7 +751,7 @@ let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
-let declare_fix boxed kind f def t =
+let declare_fix boxed kind f def t imps =
   let ce = {
     const_entry_body = def;
     const_entry_type = Some t;
@@ -750,7 +759,11 @@ let declare_fix boxed kind f def t =
     const_entry_boxed = boxed
   } in
   let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
-  ConstRef kn
+  let gr = ConstRef kn in
+    if Impargs.is_implicit_args () || imps <> [] then
+      declare_manual_implicits false gr (Impargs.is_implicit_args ()) imps;
+    gr
+
 
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
@@ -766,6 +779,7 @@ let compute_possible_guardness_evidences (n,_) fixl fixtype =
 	 but doing it properly involves delta-reduction, and it finally 
          doesn't seem to worth the effort (except for huge mutual 
 	 fixpoints ?) *)
+      (* FIXME, local_binders_length does not give the size of the final product if typeclasses are used *)
       let m = local_binders_length fixl.fix_binders in
       let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
       list_map_i (fun i _ -> i) 0 ctx
@@ -778,6 +792,11 @@ let interp_recursive fixkind l boxed =
 
   (* Interp arities allowing for unresolved types *)
   let evdref = ref (Evd.create_evar_defs Evd.empty) in
+  let fiximps = 
+    List.map 
+      (fun x -> Implicit_quantifiers.implicits_of_binders x.fix_binders) 
+      fixl 
+  in
   let fixctxs = List.map (interp_fix_context evdref env) fixl in
   let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
@@ -816,7 +835,7 @@ let interp_recursive fixkind l boxed =
   in
 
   (* Declare the recursive definitions *)
-  ignore (list_map3 (declare_fix boxed kind) fixnames fixdecls fixtypes);
+  ignore (list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps);
   if_verbose ppnl (recursive_message kind indexes fixnames);
 
   (* Declare notations *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 3f7e502850..6b15479d77 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -32,7 +32,7 @@ open Redexpr
 
 val declare_definition : identifier -> definition_kind ->
   local_binder list -> red_expr option -> constr_expr ->
-    constr_expr option -> declaration_hook -> unit
+  constr_expr option -> declaration_hook -> unit
 
 val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit
 
@@ -43,6 +43,16 @@ val declare_assumption : identifier located list ->
   coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> bool 
   ->unit
 
+val compute_interning_datas :  Environ.env ->
+    'a list ->
+    'b list ->
+    Term.types list ->
+    'a list *
+    ('b *
+     (Names.identifier list * Impargs.implicits_list *
+      Topconstr.scope_name option list))
+    list
+
 val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit
 
 val declare_mutual_with_eliminations :
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 8d9eabd7ef..95ffeb44af 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -71,6 +71,7 @@ let hm2 s =
 (* The list of all theories in the standard library /!\ order does matter *)
 let theories_dirs_map = [
     "theories/Unicode", "Unicode" ;
+    "theories/Classes", "Classes" ; 
     "theories/Program", "Program" ; 
     "theories/FSets", "FSets" ; 
     "theories/IntMap", "IntMap" ; 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index e381fe7538..128091f44d 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -21,6 +21,7 @@ open Sign
 open Environ
 open Pretype_errors
 open Type_errors
+open Typeclasses_errors
 open Indrec
 open Reduction
 open Cases
@@ -441,6 +442,38 @@ let explain_pretype_error env err =
   | NoOccurrenceFound c -> explain_no_occurrence_found env c
   | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n
 
+      
+(* Typeclass errors *)
+
+let explain_unbound_class env (_,id) =
+  str "Unbound class name " ++ Nameops.pr_id id
+
+let explain_unbound_method env cid id =
+  str "Unbound method name " ++ Nameops.pr_id (snd id) ++ spc () ++ str"of class" ++ spc () ++ 
+    Nameops.pr_id cid
+
+let pr_constr_exprs exprs = 
+  hv 0 (List.fold_right 
+	 (fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr d ++ pps)
+         exprs (mt ()))
+
+let explain_no_instance env (_,id) l =
+  str "No instance found for class " ++ Nameops.pr_id id ++ spc () ++
+  str "applied to arguments" ++ spc () ++ 
+    prlist_with_sep pr_spc (pr_lconstr_env env) l
+
+let explain_mismatched_contexts env c i j = 
+  str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
+    hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_named_context env j) ++ fnl () ++ brk (1,1) ++ 
+    hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i)
+
+let explain_typeclass_error env err = 
+  match err with
+    | UnboundClass id -> explain_unbound_class env id
+    | UnboundMethod (cid, id) -> explain_unbound_method env cid id
+    | NoInstance (id, l) -> explain_no_instance env id l
+    | MismatchedContextInstance (c, i, j) -> explain_mismatched_contexts env c i j
+	
 (* Refiner errors *)
 
 let explain_refiner_bad_type arg ty conclty =
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 05a52b8b75..d7a72bedee 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -15,6 +15,7 @@ open Indtypes
 open Environ
 open Type_errors
 open Pretype_errors
+open Typeclasses_errors
 open Indrec
 open Cases
 open Logic
@@ -28,6 +29,8 @@ val explain_pretype_error : env -> pretype_error -> std_ppcmds
 
 val explain_inductive_error : inductive_error -> std_ppcmds
 
+val explain_typeclass_error : env -> typeclass_error -> Pp.std_ppcmds 
+
 val explain_recursion_scheme_error : recursion_scheme_error -> std_ppcmds
 
 val explain_refiner_error : refiner_error -> std_ppcmds
diff --git a/toplevel/record.ml b/toplevel/record.ml
index e80001d256..73e4e42f73 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -228,4 +228,5 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
   let kinds,sp_projs = declare_projections rsp coers fields in
   let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *)
   if is_coe then Class.try_add_new_coercion build Global;
-  Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs)
+  Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
+  kn
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 5074719bc1..e322dcfd0b 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -25,4 +25,4 @@ val declare_projections :
 
 val definition_structure :
   lident with_coercion * local_binder list *
-  (local_decl_expr with_coercion) list * identifier * sorts -> unit
+  (local_decl_expr with_coercion) list * identifier * sorts -> kernel_name
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b71f9767ef..0aea24d47d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -486,7 +486,7 @@ let vernac_record struc binders sort nameopt cfs =
     | Sort s -> s
     | _ -> user_err_loc
         (constr_loc sort,"definition_structure", str "Sort expected") in
-  Record.definition_structure (struc,binders,cfs,const,s)
+  ignore(Record.definition_structure (struc,binders,cfs,const,s))
 
   (* Sections *)
 
@@ -522,6 +522,22 @@ let vernac_identity_coercion stre id qids qidt =
   let source = cl_of_qualid qids in
   Class.try_add_new_identity_coercion id stre source target
 
+(* Type classes *)
+let vernac_class id par ar sup props =
+  Classes.new_class id par ar sup props
+
+let vernac_instance sup inst props =
+  Classes.new_instance sup inst props
+
+let vernac_context l =
+  Classes.context l
+
+let vernac_declare_instance id =
+  Classes.declare_instance id
+
+(* Default tactics for solving evars management. *)
+let vernac_set_instantiation_tac tac =
+  Classes.set_instantiation_tactic tac
 
 (***********)
 (* Solving *)
@@ -656,9 +672,10 @@ let vernac_hints = Auto.add_hints
 
 let vernac_syntactic_definition = Command.syntax_definition 
 
-let vernac_declare_implicits local r = function
+let vernac_declare_implicits local r e = function
   | Some imps ->
-      Impargs.declare_manual_implicits local (global_with_alias r) imps
+      Impargs.declare_manual_implicits local (global_with_alias r) e
+	(List.map (fun (ex,b,f) -> ex, (b,f)) imps)
   | None -> 
       Impargs.declare_implicits local (global_with_alias r)
 
@@ -712,6 +729,14 @@ let _ =
       optread  = Impargs.is_contextual_implicit_args;
       optwrite = Impargs.make_contextual_implicit_args }
 
+(* let _ = *)
+(*   declare_bool_option  *)
+(*     { optsync  = true; *)
+(*       optname  = "forceable implicit arguments"; *)
+(*       optkey   = (SecondaryTable ("Forceable","Implicit")); *)
+(*       optread  = Impargs.is_forceable_implicit_args; *)
+(*       optwrite = Impargs.make_forceable_implicit_args } *)
+
 let _ =
   declare_bool_option 
     { optsync  = true;
@@ -945,6 +970,8 @@ let vernac_print = function
   | PrintOpaqueName qid -> msg (print_opaque_name qid)
   | PrintGraph -> ppnl (Prettyp.print_graph())
   | PrintClasses -> ppnl (Prettyp.print_classes())
+  | PrintTypeClasses -> ppnl (Prettyp.print_typeclasses())
+  | PrintInstances c -> ppnl (Prettyp.print_instances c)
   | PrintLtac qid -> ppnl (Tacinterp.print_ltac (snd (qualid_of_reference qid)))
   | PrintCoercions -> ppnl (Prettyp.print_coercions())
   | PrintCoercionPaths (cls,clt) ->
@@ -1188,6 +1215,15 @@ let interp c = match c with
   | VernacCoercion (str,r,s,t) -> vernac_coercion str r s t
   | VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t
 
+  (* Type classes *)
+  | VernacClass (id, par, ar, sup, props) -> vernac_class id par ar sup props
+
+  | VernacInstance (sup, inst, props) -> vernac_instance sup inst props
+  | VernacContext sup -> vernac_context sup
+  | VernacDeclareInstance id -> vernac_declare_instance id
+
+  | VernacSetInstantiationTactic (tac) -> vernac_set_instantiation_tac tac
+
   (* Solving *)
   | VernacSolve (n,tac,b) -> vernac_solve n tac b
   | VernacSolveExistential (n,c) -> vernac_solve_existential n c
@@ -1222,7 +1258,7 @@ let interp c = match c with
   | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
   | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
   | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
-  | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
+  | VernacDeclareImplicits (local,qid,e,l) ->vernac_declare_implicits local qid e l
   | VernacReserve (idl,c) -> vernac_reserve idl c
   | VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl
   | VernacSetOption (key,v) -> vernac_set_option key v
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index c893933015..a5c04a5611 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -48,6 +48,8 @@ type printable =
   | PrintOpaqueName of reference
   | PrintGraph
   | PrintClasses
+  | PrintTypeClasses
+  | PrintInstances of reference
   | PrintLtac of reference
   | PrintCoercions
   | PrintCoercionPaths of class_rawexpr * class_rawexpr
@@ -145,10 +147,12 @@ type sort_expr = Rawterm.rawsort
 
 type decl_notation = (string * constr_expr * scope_name option) option
 type simple_binder = lident list  * constr_expr
+type class_binder = lident * constr_expr list
 type 'a with_coercion = coercion_flag * 'a
 type constructor_expr = (lident * constr_expr) with_coercion
 type inductive_expr =
      lident * local_binder list * constr_expr * constructor_expr list
+
 type definition_expr =
   | ProveBody of local_binder list * constr_expr
   | DefineBody of local_binder list * raw_red_expr option * constr_expr
@@ -220,6 +224,26 @@ type vernac_expr =
   | VernacIdentityCoercion of strength * lident * 
       class_rawexpr * class_rawexpr
 
+  (* Type classes *)
+  | VernacClass of
+      lident * (* name *)
+	(lident * constr_expr) list * (* params *)
+	sort_expr located * (* arity *)
+	typeclass_context * (* super *)
+	(lident * constr_expr) list (* props *)
+	
+  | VernacInstance of
+      typeclass_context * (* super *)
+	typeclass_constraint * (* instance name, class name, params *)
+	(lident * lident list * constr_expr) list (* props *)
+
+  | VernacContext of typeclass_context
+	
+  | VernacDeclareInstance of
+      lident (* instance name *)
+
+  | VernacSetInstantiationTactic of raw_tactic_expr
+
   (* Modules and Module Types *)
   | VernacDeclareModule of bool option * lident * 
       module_binder list * (module_type_ast * bool)
@@ -260,12 +284,12 @@ type vernac_expr =
 
   (* Commands *)
   | VernacDeclareTacticDefinition of
-      rec_flag * (lident * raw_tactic_expr) list
+      rec_flag * (lident * bool * raw_tactic_expr) list
   | VernacHints of locality_flag * lstring list * hints
   | VernacSyntacticDefinition of identifier * constr_expr * locality_flag *
       onlyparsing_flag
-  | VernacDeclareImplicits of locality_flag * lreference *
-      (explicitation * bool) list option
+  | VernacDeclareImplicits of locality_flag * lreference * bool *
+      (explicitation * bool * bool) list option
   | VernacReserve of lident list * constr_expr
   | VernacSetOpacity of opacity_flag * lreference list
   | VernacUnsetOption of Goptions.option_name
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index c7a9774e09..d76c281be1 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -151,12 +151,12 @@ let rec uri_of_constr c =
       let inst,rest = merge (section_parameters f) args in
       uri_of_constr f; url_char ' '; uri_params uri_of_constr inst; 
       url_list_with_sep " " uri_of_constr rest
-  | RLambda (_,na,ty,c) ->
+  | RLambda (_,na,k,ty,c) ->
       url_string "\\lambda "; url_of_name na; url_string ":";
       uri_of_constr ty; url_string "."; uri_of_constr c
-  | RProd (_,Anonymous,ty,c) ->
+  | RProd (_,Anonymous,k,ty,c) ->
       uri_of_constr ty; url_string "\\to "; uri_of_constr c
-  | RProd (_,Name id,ty,c) ->
+  | RProd (_,Name id,k,ty,c) ->
       url_string "\\forall "; url_id id; url_string ":";
       uri_of_constr ty; url_string "."; uri_of_constr c
   | RLetIn (_,na,b,c) ->