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

14 files changed, 447 insertions, 142 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index d1b4b50ebd..9cb65f76e0 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -121,7 +121,7 @@ let rec chop_product n t =
       | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
       | _ -> None
 
-let eterm_obligations env name isevars evm fs t tycon = 
+let eterm_obligations env name isevars evm fs t ty = 
   (* 'Serialize' the evars, we assume that the types of the existentials
      refer to previous existentials in the list only *)
   trace (str " In eterm: isevars: " ++ my_print_evardefs isevars);
@@ -165,6 +165,7 @@ let eterm_obligations env name isevars evm fs t tycon =
   let t', _, transparent = (* Substitute evar refs in the term by variables *)
     subst_evar_constr evts 0 t 
   in
+  let ty, _, _ = subst_evar_constr evts 0 ty in
   let evars = 
     List.map (fun (_, ((_, name), _, opaque, typ, deps)) -> name, typ, not (opaque = None) && not (Idset.mem name transparent), deps) evts
   in
@@ -177,7 +178,7 @@ let eterm_obligations env name isevars evm fs t tycon =
 			    Termops.print_constr_env (Global.env ()) typ))
 		evars);
      with _ -> ());
-    Array.of_list (List.rev evars), t'
+    Array.of_list (List.rev evars), t', ty
 
 let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
 
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index a2582c5ca0..e23fd535ca 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -19,9 +19,9 @@ val mkMetas : int -> constr list
 (* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *)
 
 (* env, id, evars, number of
-   function prototypes to try to clear from evars contexts, object and optional type *)
-val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> constr -> types option -> 
-  (identifier * types * bool * Intset.t) array * constr
+   function prototypes to try to clear from evars contexts, object and type *)
+val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> constr -> types -> 
+  (identifier * types * bool * Intset.t) array * constr * types
     (* Obl. name, type as product, opacity (true = opaque) and dependencies as indexes into the array *)
 
 val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index c2691c781c..49e312aeb6 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -44,17 +44,20 @@ struct
   let subtac_nameopt : identifier option Gram.Entry.e = gec "subtac_nameopt"
 end
 
+open Rawterm
 open SubtacGram 
 open Util
 open Pcoq
-
+open Prim
+open Constr
 let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
 
 GEXTEND Gram
-  GLOBAL: subtac_gallina_loc Constr.binder_let Constr.binder subtac_nameopt;
+  GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder_let Constr.binder subtac_nameopt;
  
   subtac_gallina_loc:
-    [ [ g = Vernac.gallina -> loc, g ] ]
+    [ [ g = Vernac.gallina -> loc, g
+    | g = Vernac.gallina_ext -> loc, g ] ]
     ;
 
   subtac_nameopt:
@@ -63,18 +66,18 @@ GEXTEND Gram
     ;
 
   Constr.binder_let:
-    [ [ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> 
-	  let typ = mkAppC (sigref, [mkLambdaC ([id], t, c)]) in
-	    LocalRawAssum ([id], typ)
+    [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> 
+	  let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
+	    LocalRawAssum ([id], default_binder_kind, typ)
     ] ];
 
   Constr.binder:
     [ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" ->
-          ([id],mkAppC (sigref, [mkLambdaC ([id], c, p)]))
+          ([id],default_binder_kind, mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, c, p)]))
       | "("; id=Prim.name; ":"; c=Constr.lconstr; ")" ->
-          ([id],c)
+          ([id],default_binder_kind, c)
       | "("; id=Prim.name; lid=LIST1 Prim.name; ":"; c=Constr.lconstr; ")" ->
-          (id::lid,c)
+          (id::lid,default_binder_kind, c)
     ] ];
 
   END
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 4f5e302c22..56ebc4f522 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -49,6 +49,22 @@ open Decl_kinds
 open Tacinterp
 open Tacexpr
 
+let solve_tccs_in_type env id isevars evm c typ =
+  if not (evm = Evd.empty) then 
+    let stmt_id = Nameops.add_suffix id "_stmt" in
+    let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 c typ in
+    (** Make all obligations transparent so that real dependencies can be sorted out by the user *)
+    let obls = Array.map (fun (id, t, op, d) -> (id, t, false, d)) obls in
+      match Subtac_obligations.add_definition stmt_id c' typ obls with
+	  Subtac_obligations.Defined cst -> constant_value (Global.env()) cst
+	| _ -> 
+	    errorlabstrm "start_proof" 
+	      (str "The statement obligations could not be resolved automatically, " ++ spc () ++
+		  str "write a statement definition first.")
+  else
+    let _ = Typeops.infer_type env c in c
+
+
 let start_proof_com env isevars sopt kind (bl,t) hook =
   let id = match sopt with
     | Some id ->
@@ -60,21 +76,11 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
 	next_global_ident_away false (id_of_string "Unnamed_thm")
  	  (Pfedit.get_all_proof_names ())
   in
-  let evm, c, typ = 
+  let evm, c, typ, _imps = 
     Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None 
   in
-    if not (evm = Evd.empty) then 
-      let stmt_id = Nameops.add_suffix id "_stmt" in
-      let obls, c' = eterm_obligations env stmt_id !isevars evm 0 c (Some typ) in
-	match Subtac_obligations.add_definition stmt_id c' typ obls with
-	    Subtac_obligations.Defined cst -> Command.start_proof id kind (constant_value (Global.env()) cst) hook
-	  | _ -> 
-	      errorlabstrm "start_proof" 
-		(str "The statement obligations could not be resolved automatically, " ++ spc () ++
-		    str "write a statement definition first.")
-    else
-      let _ = Typeops.infer_type env c in
-	Command.start_proof id kind c hook
+  let c = solve_tccs_in_type env id isevars evm c typ in
+    Command.start_proof id kind c hook	
       
 let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
 
@@ -88,10 +94,12 @@ let assumption_message id =
   Flags.if_verbose message ((string_of_id id) ^ " is assumed")
 
 let declare_assumption env isevars idl is_coe k bl c nl =
-  if not (Pfedit.refining ()) then 
-    let evm, c, typ = 
-      Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None 
+  if not (Pfedit.refining ()) then
+    let id = snd (List.hd idl) in
+    let evm, c, typ, imps = 
+      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 nl) idl
   else
     errorlabstrm "Command.Assumption"
@@ -114,8 +122,13 @@ let subtac (loc, command) =
   match command with
 	VernacDefinition (defkind, (locid, id), expr, hook) -> 
 	    (match expr with
-		 ProveBody (bl, c) -> ignore(Subtac_pretyping.subtac_proof env isevars id bl c None)
-	       | DefineBody (bl, _, c, tycon) -> 
+	      | ProveBody (bl, t) -> 
+		  if Lib.is_modtype () then
+		    errorlabstrm "Subtac_command.StartProof"
+		      (str "Proof editing mode not supported in module types");
+		  start_proof_and_print env isevars (Some id) (Global, DefinitionBody Definition) (bl,t) 
+		    (fun _ _ -> ())
+	      | DefineBody (bl, _, c, tycon) -> 
 		   ignore(Subtac_pretyping.subtac_proof env isevars id bl c tycon))
       | VernacFixpoint (l, b) -> 
 	  let _ = trace (str "Building fixpoint") in
@@ -135,6 +148,9 @@ let subtac (loc, command) =
       | VernacAssumption (stre,nl,l) -> 
 	  vernac_assumption env isevars stre l nl
 
+      | VernacInstance (sup, is, props) ->
+	  Subtac_classes.new_instance sup is props
+
 (*       | VernacCoFixpoint (l, b) ->  *)
 (* 	  let _ = trace (str "Building cofixpoint") in *)
 (* 	    ignore(Subtac_command.build_recursive l b) *)
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 34c398289a..e46ca822ee 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1395,9 +1395,9 @@ let set_arity_signature dep n arsign tomatchl pred x =
   let rec decomp_lam_force n avoid l p =
     if n = 0 then (List.rev l,p,avoid) else
     match p with
-      | RLambda (_,(Name id as na),_,c) -> 
+      | RLambda (_,(Name id as na),k,_,c) -> 
           decomp_lam_force (n-1) (id::avoid) (na::l) c
-      | RLambda (_,(Anonymous as na),_,c) -> decomp_lam_force (n-1) avoid (na::l) c
+      | RLambda (_,(Anonymous as na),k,_,c) -> decomp_lam_force (n-1) avoid (na::l) c
       | _ ->
           let x = next_ident_away (id_of_string "x") avoid in
           decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
@@ -2091,13 +2091,12 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
 (*   let env = nf_evars_env !isevars (env : env) in *)
 (*      trace (str "Evars : " ++ my_print_evardefs !isevars); *)
 (*     trace (str "Env : " ++ my_print_env env); *)
-    
-  let tomatchs, tomatchs_lets = abstract_tomatch env tomatchs in
-  let tomatchs_len = List.length tomatchs_lets in
-  let tycon = lift_tycon tomatchs_len tycon in
-  let env = push_rel_context tomatchs_lets env in
   let _isdep = List.exists (fun (x, y) -> is_dependent_ind y) tomatchs in
     if predopt = None then
+      let tomatchs, tomatchs_lets = abstract_tomatch env tomatchs in
+      let tomatchs_len = List.length tomatchs_lets in
+      let tycon = lift_tycon tomatchs_len tycon in
+      let env = push_rel_context tomatchs_lets env in
       let len = List.length eqns in 
       let sign, allnames, signlen, eqs, neqs, args = 
 	(* The arity signature *)
@@ -2185,7 +2184,6 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
 	  let j = compile pb in
 	  (* We check for unused patterns *)
 	  List.iter (check_unused_pattern env) matx;
-	  let j = { j with uj_val = it_mkLambda_or_LetIn j.uj_val tomatchs_lets } in
 	    inh_conv_coerce_to_tycon loc env isevars j tycon	  
 
 end
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
new file mode 100644
index 0000000000..da91b04062
--- /dev/null
+++ b/contrib/subtac/subtac_classes.ml
@@ -0,0 +1,187 @@
+(************************************************************************)
+(*  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*)
+
+open Pretyping
+open Evd
+open Environ
+open Term
+open Rawterm
+open Topconstr
+open Names
+open Libnames
+open Pp
+open Vernacexpr
+open Constrintern
+open Subtac_command
+open Typeclasses
+open Typeclasses_errors
+open Termops
+open Decl_kinds
+open Entries
+
+module SPretyping = Subtac_pretyping.Pretyping
+
+let interp_binder_evars evdref env na t =
+  let t = Constrintern.intern_gen true (Evd.evars_of !evdref) env t in
+    SPretyping.understand_tcc_evars evdref env IsType t
+
+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, cl) -> 
+      let t' = interp_binder_evars isevars env (snd iid) cl 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 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 new_instance sup  (instid, bk, cl) props =
+  let id, par = Implicit_quantifiers.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 gen_ctx = 
+    let is_free ((_, x), _) = 
+      let f l = not (List.exists (fun ((_, y), _) -> y = x) l) in
+      let g l = not (List.exists (fun ((_, y), _, _) -> y = Name x) l) in
+	f gen_ctx && g sup
+    in
+    let parbinders = Implicit_quantifiers.compute_constrs_freevars_binders (vars_of_env env) par in
+    let parbinders' = List.filter is_free parbinders in
+      gen_ctx @ parbinders'
+  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 
+	    Classes.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
+	  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 substctx = Typeclasses.nf_substitution sigma subst in
+  let subst, _propsctx = 
+    let props = 
+      List.map (fun (x, l, d) -> 
+	x, Topconstr.abstract_constr_expr d (Classes.binders_of_lidents l))
+	props
+    in
+      if List.length props > List.length k.cl_props then 
+	Classes.mismatched_props env' (List.map snd props) k.cl_props;
+      let props, rest = 
+	List.fold_left
+	  (fun (props, rest) (id,_,_) -> 
+	    try 
+	      let (_, c) = List.find (fun ((_,id'), c) -> id' = id) rest in
+	      let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
+		c :: props, rest'
+	    with Not_found -> (CHole Util.dummy_loc :: props), rest)
+	  ([], props) k.cl_props
+      in
+	if rest <> [] then 
+	  unbound_method env k.cl_name (fst (List.hd rest))
+	else
+	  type_ctx_instance isevars env' k.cl_props props substctx
+  in
+  let app = 
+    applistc (mkConstruct (k.cl_impl, 1)) (List.rev_map snd subst)
+  in 
+  let term = it_mkNamedLambda_or_LetIn (it_mkNamedLambda_or_LetIn app supctx) genctx in
+  isevars := Evarutil.nf_evar_defs !isevars;
+  let term = Evarutil.nf_isevar !isevars term in
+  let termtype = 
+    let app = applistc (mkInd (k.cl_impl)) (List.rev_map snd substctx) in
+    let t = it_mkNamedProd_or_LetIn (it_mkNamedProd_or_LetIn app supctx) genctx in
+      Evarutil.nf_isevar !isevars t
+  in
+  isevars := undefined_evars !isevars;
+  let id =
+    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
+  let imps = 
+    Util.list_map_i 
+      (fun i (na, b, t) -> ExplByPos (i, Some na), (true, true))
+      1 (genctx @ List.rev supctx)
+  in
+  let hook cst = 
+    let inst = 
+      { is_class = k;
+	is_name = id;
+(* 	is_params = paramsctx; *)
+(* 	is_super = superctx; *)
+	is_impl = cst;
+(* 	is_add_hint = (fun () -> Classes.add_instance_hint id); *)
+      }
+    in
+      Classes.add_instance_hint id;
+      Impargs.declare_manual_implicits false (ConstRef cst) false imps;
+      Typeclasses.add_instance inst
+  in
+  let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in
+  let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
+    ignore (Subtac_obligations.add_definition id constr typ ~kind:Instance ~hook obls)
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
new file mode 100644
index 0000000000..ce4b32cad8
--- /dev/null
+++ b/contrib/subtac/subtac_classes.mli
@@ -0,0 +1,39 @@
+(************************************************************************)
+(*  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
+open Classes
+(*i*)
+
+val type_ctx_instance :     Evd.evar_defs ref ->
+    Environ.env ->
+    (Names.identifier * 'a * Term.constr) list ->
+    Topconstr.constr_expr list ->
+    (Names.identifier * Term.constr) list ->
+    (Names.identifier * Term.constr) list *
+    (Names.identifier * Term.constr option * Term.constr) list
+
+val new_instance : 
+  typeclass_context ->
+  typeclass_constraint ->
+  binder_def_list ->
+  unit
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index a9a30c57af..9afa6f0675 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -98,11 +98,11 @@ let interp_binder sigma env na t =
 let interp_context sigma env params = 
   List.fold_left
     (fun (env,params) d -> match d with
-      | LocalRawAssum ([_,na],(CHole _ as t)) ->
+      | LocalRawAssum ([_,na],k,(CHole _ as t)) ->
 	  let t = interp_binder sigma env na t in
 	  let d = (na,None,t) in
 	  (push_rel d env, d::params)
-      | LocalRawAssum (nal,t) ->
+      | LocalRawAssum (nal,k,t) ->
 	  let t = interp_type sigma env t in
 	  let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
 	  let ctx = List.rev ctx in
@@ -152,7 +152,7 @@ let collect_non_rec env =
 let list_of_local_binders l = 
   let rec aux acc = function
       Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl
-    | Topconstr.LocalRawAssum (nl, c) :: tl -> 
+    | Topconstr.LocalRawAssum (nl, k, c) :: tl -> 
 	aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl
     | [] -> List.rev acc
   in aux [] l
@@ -294,12 +294,11 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 		    lift lift_cst prop ;
 		    lift lift_cst intern_body_lam |])
       | Some f ->
-	  lift (succ after_length) 
-	    (mkApp (constr_of_global (Lazy.force fix_measure_sub_ref), 
-		    [| argtyp ; 
-		       f ;
-		       lift lift_cst prop ;
-		       lift lift_cst intern_body_lam |]))
+	  mkApp (constr_of_global (Lazy.force fix_measure_sub_ref), 
+		[| lift lift_cst argtyp ; 
+		   lift lift_cst f ;
+		   lift lift_cst prop ;
+		   lift lift_cst intern_body_lam |])
   in
   let def_appl = applist (fix_def, gen_rels (after_length + 1)) in
   let def = it_mkLambda_or_LetIn def_appl binders_rel in
@@ -316,13 +315,13 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let evm = non_instanciated_map env isevars evm in
 
     (*   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in *)
-  let evars, evars_def = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc (Some fullctyp) in
+  let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in
     (*     (try trace (str "Generated obligations : "); *)
 (*        Array.iter *)
     (* 	 (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) *)
     (* 	 evars; *)
     (*      with _ -> ());     *)
-    Subtac_obligations.add_definition recname evars_def fullctyp evars
+    Subtac_obligations.add_definition recname evars_def evars_typ evars
 
 let nf_evar_context isevars ctx = 
   List.map (fun (n, b, t) -> 
@@ -412,11 +411,12 @@ let build_mutrec lnameargsardef boxed =
 	(* Generalize by the recursive prototypes  *)
       let def = 
 	Termops.it_mkNamedLambda_or_LetIn def rec_sign
-      and typ = 
+      and typ =
 	Termops.it_mkNamedProd_or_LetIn typ rec_sign
       in
-      let evm = Subtac_utils.evars_of_term evm Evd.empty def in
-      let evars, def = Eterm.eterm_obligations env id isevars evm recdefs def (Some typ) in
+      let evm' = Subtac_utils.evars_of_term evm Evd.empty def in
+      let evm' = Subtac_utils.evars_of_term evm evm' typ in
+      let evars, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in
 	collect_evars (succ i) ((id, def, typ, evars) :: acc)
     else acc
   in 
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index e3cf7a57a5..c184169ac7 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -12,6 +12,8 @@ open Decl_kinds
 open Util
 open Evd
 
+type definition_hook = constant -> unit
+
 let pperror cmd = Util.errorlabstrm "Program" cmd
 let error s = pperror (str s)
 
@@ -40,6 +42,9 @@ type program_info = {
   prg_obligations: obligations;
   prg_deps : identifier list;
   prg_nvrec : int array;
+  prg_implicits : (Topconstr.explicitation * (bool * bool)) list;
+  prg_kind : definition_object_kind;
+  prg_hook : definition_hook;
 }
 
 let assumption_message id =
@@ -106,7 +111,7 @@ let progmap_union = ProgMap.fold ProgMap.add
 
 let cache (_, (infos, tac)) =
   from_prg := infos;
-  default_tactic_expr := tac
+  set_default_tactic tac
 
 let (input,output) = 
   declare_object
@@ -125,24 +130,30 @@ let rec intset_to = function
   
 let subst_body prg = 
   let obls, _ = prg.prg_obligations in
-    subst_deps obls (intset_to (pred (Array.length obls))) prg.prg_body
-
+  let ints = intset_to (pred (Array.length obls)) in
+    subst_deps obls ints prg.prg_body,
+  subst_deps obls ints (Termops.refresh_universes prg.prg_type)
+    
 let declare_definition prg =
-  let body = subst_body prg in
+  let body, typ = subst_body prg in
     (try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
 		  my_print_constr (Global.env()) body ++ str " : " ++ 
 		  my_print_constr (Global.env()) prg.prg_type);
      with _ -> ());
   let ce = 
     { const_entry_body = body;
-      const_entry_type = Some (Termops.refresh_universes prg.prg_type);
+      const_entry_type = Some typ;
       const_entry_opaque = false;
       const_entry_boxed = false} 
   in
   let c = Declare.declare_constant 
-    prg.prg_name (DefinitionEntry ce,IsDefinition Definition)
+    prg.prg_name (DefinitionEntry ce,IsDefinition prg.prg_kind)
   in
+  let gr = ConstRef c in
+    if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
+      Impargs.declare_manual_implicits false gr (Impargs.is_implicit_args ()) prg.prg_implicits;
     print_message (definition_message c);
+    prg.prg_hook c;
     c
 
 open Pp
@@ -151,14 +162,18 @@ open Ppconstr
 let declare_mutual_definition l =
   let len = List.length l in
   let namerec = Array.of_list (List.map (fun x -> x.prg_name) l) in
-  let arrec = 
-    Array.of_list (List.map (fun x -> snd (decompose_prod_n len x.prg_type)) l)
-  in
-  let recvec = 
-    Array.of_list 
-      (List.map (fun x -> 
-		   let subs = (subst_body x) in
-		     snd (decompose_lam_n len subs)) l)
+(*   let arrec =  *)
+(*     Array.of_list (List.map (fun x -> snd (decompose_prod_n len x.prg_type)) l) *)
+(*   in *)
+  let recvec, arrec = 
+    let l, l' = 
+      List.split
+	(List.map (fun x -> 
+	  let subs, typ = (subst_body x) in
+	    snd (decompose_lam_n len subs), 
+	  snd (decompose_prod_n len typ)) l)
+    in
+      Array.of_list l, Array.of_list l'
   in
   let nvrec = (List.hd l).prg_nvrec in
   let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
@@ -205,7 +220,7 @@ let try_tactics obls =
         
 let red = Reductionops.nf_betaiota
 
-let init_prog_info n b t deps nvrec obls =
+let init_prog_info n b t deps nvrec obls impls kind hook =
   let obls' = 
     Array.mapi
       (fun i (n, t, o, d) ->
@@ -216,7 +231,7 @@ let init_prog_info n b t deps nvrec obls =
       obls
   in
     { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
-      prg_deps = deps; prg_nvrec = nvrec; }
+      prg_deps = deps; prg_nvrec = nvrec; prg_implicits = impls; prg_kind = kind; prg_hook = hook; }
     
 let get_prog name =
   let prg_infos = !from_prg in
@@ -327,7 +342,8 @@ let rec solve_obligation prg num =
 		       | _ -> ());
 	      trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
 		       Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
-	      Pfedit.by !default_tactic
+	      Pfedit.by !default_tactic;
+	      Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
 	| l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
 			++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
 
@@ -393,9 +409,22 @@ and auto_solve_obligations n : progress =
   Flags.if_verbose msgnl (str "Solving obligations automatically...");
   try solve_obligations n !default_tactic with NoObligations _ -> Dependent
       
-let add_definition n b t obls =
+open Pp
+let show_obligations ?(msg=true) n =
+  let prg = get_prog_err n in
+  let n = prg.prg_name in
+  let obls, rem = prg.prg_obligations in
+    if msg then msgnl (int rem ++ str " obligation(s) remaining: ");
+    Array.iteri (fun i x -> 
+		   match x.obl_body with 
+		       None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ 
+					my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())
+		    | Some _ -> ())
+      obls
+
+let add_definition n b t ?(implicits=[]) ?(kind=Definition) ?(hook=fun x -> ()) obls =
   Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
-  let prg = init_prog_info n b t [] (Array.make 0 0) obls in
+  let prg = init_prog_info n b t [] (Array.make 0 0) obls implicits kind hook in
   let obls,_ = prg.prg_obligations in
   if Array.length obls = 0 then (
     Flags.if_verbose ppnl (str ".");    
@@ -406,19 +435,30 @@ let add_definition n b t obls =
     let len = Array.length obls in
     let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
       from_prg := ProgMap.add n prg !from_prg; 
-      auto_solve_obligations (Some n))
+      let res = auto_solve_obligations (Some n) in
+	match res with
+	  | Remain rem when rem < 5 -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
+	  | _ -> res)
 	
-let add_mutual_definitions l nvrec =
+let add_mutual_definitions l ?(implicits=[]) ?(kind=Definition) nvrec =
   let deps = List.map (fun (n, b, t, obls) -> n) l in
   let upd = List.fold_left
       (fun acc (n, b, t, obls) ->
-	 let prg = init_prog_info n b t deps nvrec obls in
+	 let prg = init_prog_info n b t deps nvrec obls implicits kind (fun x -> ()) in
 	   ProgMap.add n prg acc)
       !from_prg l
   in
     from_prg := upd;
-    List.iter (fun x -> ignore(auto_solve_obligations (Some x))) deps
-
+    let _defined = 
+      List.fold_left (fun finished x -> 
+	if finished then finished 
+	else
+	  match auto_solve_obligations (Some x) with
+	      Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true
+	    | _ -> false) 
+	false deps
+    in ()
+	
 let admit_obligations n =
   let prg = get_prog_err n in
   let obls, rem = prg.prg_obligations in
@@ -447,18 +487,5 @@ let next_obligation n =
     array_find (fun x ->  x.obl_body = None && deps_remaining obls x.obl_deps = [])
       obls
   in solve_obligation prg i
-      
-open Pp
-let show_obligations n =
-  let prg = get_prog_err n in
-  let n = prg.prg_name in
-  let obls, rem = prg.prg_obligations in
-    msgnl (int rem ++ str " obligation(s) remaining: ");
-    Array.iteri (fun i x -> 
-		   match x.obl_body with 
-		       None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ 
-					my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())
-		    | Some _ -> ())
-      obls
-			
+      			
 let default_tactic () = !default_tactic
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index cd70d5233d..30fbd02843 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -12,11 +12,18 @@ type progress = (* Resolution status of a program *)
 val set_default_tactic : Tacexpr.glob_tactic_expr -> unit
 val default_tactic : unit -> Proof_type.tactic
 
+type definition_hook = constant -> unit
+
 val add_definition : Names.identifier ->  Term.constr -> Term.types -> 
-  obligation_info -> progress
+  ?implicits:(Topconstr.explicitation * (bool * bool)) list ->
+  ?kind:Decl_kinds.definition_object_kind ->
+  ?hook:definition_hook -> obligation_info -> progress
 
 val add_mutual_definitions : 
-  (Names.identifier * Term.constr * Term.types * obligation_info) list -> int array -> unit
+  (Names.identifier * Term.constr * Term.types * obligation_info) list -> 
+  ?implicits:(Topconstr.explicitation * (bool * bool)) list ->
+  ?kind:Decl_kinds.definition_object_kind ->
+  int array -> unit
 
 val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit
 
@@ -31,7 +38,7 @@ val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic -
 
 val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
 
-val show_obligations : Names.identifier option -> unit
+val show_obligations : ?msg:bool -> Names.identifier option -> unit
 
 val admit_obligations : Names.identifier option -> unit
 
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index a0e7e6951c..0703bcb837 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -70,7 +70,12 @@ let merge_evms x y =
 
 let interp env isevars c tycon = 
   let j = pretype tycon env isevars ([],[]) c in
-  let evm = evars_of !isevars in    
+  let _ = isevars := Evarutil.nf_evar_defs !isevars in
+  let evd,_ = consider_remaining_unif_problems env !isevars in
+  let unevd = undefined_evars evd in
+  let unevd' = Typeclasses.resolve_typeclasses env (Evd.evars_of unevd) evd in
+  let evm = evars_of unevd' in
+    isevars := unevd';
     nf_evar evm j.uj_val, nf_evar evm j.uj_type
 
 let find_with_index x l =
@@ -98,7 +103,7 @@ let env_with_binders env isevars l =
 	let coqdef, deftyp = interp env isevars rawdef empty_tycon in
 	let reldecl = (name, Some coqdef, deftyp) in
 	  aux  (push_rel reldecl env, reldecl :: rels) tl
-    | Topconstr.LocalRawAssum (bl, typ) :: tl ->
+    | Topconstr.LocalRawAssum (bl, k, typ) :: tl ->
 	let rawtyp = coqintern_type !isevars env typ in
 	let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in
 	let acc = 
@@ -111,45 +116,28 @@ let env_with_binders env isevars l =
     | [] -> acc
   in aux (env, []) l
 
-let subtac_process env isevars id l c tycon =
-  let c = Command.abstract_constr_expr c l in
-(*   let env_binders, binders_rel = env_with_binders env isevars l in *)
+let subtac_process env isevars id bl c tycon =
+(*   let bl = Implicit_quantifiers.ctx_of_class_binders (vars_of_env env) cbl @ l in *)
+  let imps = Implicit_quantifiers.implicits_of_binders bl in
+  let c = Command.abstract_constr_expr c bl in
   let tycon = 
     match tycon with
 	None -> empty_tycon
       | Some t -> 
-	  let t = Command.generalize_constr_expr t l in
+	  let t = Command.generalize_constr_expr t bl in
 	  let t = coqintern_type !isevars env t in
 	  let coqt, ttyp = interp env isevars t empty_tycon in
 	    mk_tycon coqt
   in    
   let c = coqintern_constr !isevars env c in
   let coqc, ctyp = interp env isevars c tycon in
-(*   let _ = try trace (str "Interpreted term: " ++ my_print_constr env coqc ++ spc () ++ *)
-(* 		 str "Coq type: " ++ my_print_constr env ctyp) *)
-(*   with _ -> () *)
-(*   in *)
-(*   let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars_of !isevars))  with _ -> () in *)
-    
-(*   let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel  *)
-(*   and fullctyp = it_mkProd_or_LetIn ctyp binders_rel *)
-(*   in *)
-  let fullcoqc = Evarutil.nf_evar (evars_of !isevars) coqc in
-  let fullctyp = Evarutil.nf_evar (evars_of !isevars) ctyp in
-(*   let evm = evars_of_term (evars_of !isevars) Evd.empty fullctyp in *)
-(*   let evm = evars_of_term (evars_of !isevars) evm fullcoqc in *)
-(*   let _ = try trace (str "After evar normalization remain: " ++ spc () ++ *)
-(* 		       Evd.pr_evar_map evm) *)
-(*   with _ -> () *)
-(*   in *)
   let evm = non_instanciated_map env isevars (evars_of !isevars) in
-(*   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in *)
-    evm, fullcoqc, fullctyp
+    evm, coqc, ctyp, imps
 
 open Subtac_obligations
 
-let subtac_proof env isevars id l c tycon =
-  let evm, coqc, coqt = subtac_process env isevars id l c tycon in
+let subtac_proof env isevars id bl c tycon =
+  let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in
   let evm = Subtac_utils.evars_of_term evm Evd.empty coqc in
-  let evars, def = Eterm.eterm_obligations env id !isevars evm 0 coqc (Some coqt) in
-    add_definition id def coqt evars
+  let evars, def, ty = Eterm.eterm_obligations env id !isevars evm 0 coqc coqt in
+    add_definition id def ty ~implicits:imps evars
diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli
index afe554c87e..4af37043fd 100644
--- a/contrib/subtac/subtac_pretyping.mli
+++ b/contrib/subtac/subtac_pretyping.mli
@@ -5,11 +5,19 @@ open Sign
 open Evd
 open Global
 open Topconstr
+open Implicit_quantifiers
+open Impargs
 
 module Pretyping : Pretyping.S
 
+val interp :
+    Environ.env ->
+    Evd.evar_defs ref ->
+    Rawterm.rawconstr ->
+    Evarutil.type_constraint -> Term.constr * Term.constr
+
 val subtac_process : env -> evar_defs ref -> identifier -> local_binder list ->
-  constr_expr -> constr_expr option -> evar_map * constr * types
+  constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list
 
 val subtac_proof : env -> evar_defs ref -> identifier -> local_binder list ->
   constr_expr -> constr_expr option -> Subtac_obligations.progress
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 0ed0632c65..a2d5be66c1 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -200,11 +200,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     | RRec (loc,fixkind,names,bl,lar,vdef) ->
 	let rec type_bl env ctxt = function
             [] -> ctxt
-          | (na,None,ty)::bl ->
+          | (na,k,None,ty)::bl ->
               let ty' = pretype_type empty_valcon env isevars lvar ty in
               let dcl = (na,None,ty'.utj_val) in
 		type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
-          | (na,Some bd,ty)::bl ->
+          | (na,k,Some bd,ty)::bl ->
               let ty' = pretype_type empty_valcon env isevars lvar ty in
               let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in
               let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
@@ -326,7 +326,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  | _ -> resj in
 	  inh_conv_coerce_to_tycon loc env isevars resj tycon
 
-    | RLambda(loc,name,c1,c2)      ->
+    | RLambda(loc,name,k,c1,c2)      ->
 	let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
 	let dom_valcon = valcon_of_tycon dom in
 	let j = pretype_type dom_valcon env isevars lvar c1 in
@@ -334,7 +334,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	let j' = pretype rng (push_rel var env) isevars lvar c2 in 
 	  judge_of_abstraction env name j j'
 
-    | RProd(loc,name,c1,c2)        ->
+    | RProd(loc,name,k,c1,c2)        ->
 	let j = pretype_type empty_valcon env isevars lvar c1 in
 	let var = (name,j.utj_val) in
 	let env' = push_rel_assum var env in
@@ -557,7 +557,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	    (pretype tycon env isevars lvar c).uj_val
       | IsType ->
 	  (pretype_type empty_valcon env isevars lvar c).utj_val in
-      nf_evar (evars_of !isevars) c'
+    let evd,_ = consider_remaining_unif_problems env !isevars in
+    let evd = nf_evar_defs evd in
+    let c' = nf_evar (evars_of evd) c' in
+(*     let evd = undefined_evars evd in *)
+    let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in
+    let c' = nf_evar (evars_of evd) c' in
+      isevars := evd;
+      c'
 
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
@@ -585,11 +592,16 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   let ise_pretype_gen fail_evar sigma env lvar kind c =
     let isevars = ref (Evd.create_evar_defs sigma) in
     let c = pretype_gen isevars env lvar kind c in
-    let isevars,_ = consider_remaining_unif_problems env !isevars in
-    let c = nf_evar (evars_of isevars) c in
-      if fail_evar then check_evars env sigma isevars c;
-      isevars, c
-
+(*     let evd,_ = consider_remaining_unif_problems env !isevars in *)
+(*     let evd = nf_evar_defs evd in *)
+(*     let c = nf_evar (evars_of evd) c in *)
+(*     let evd = undefined_evars evd in *)
+(*     let evd = Typeclasses.resolve_typeclasses env sigma evd in *)
+(*     let c = nf_evar (evars_of evd) c in *)
+    let evd = !isevars in
+      if fail_evar then check_evars env (Evd.evars_of evd) evd c;
+      evd, c
+	
   (** Entry points of the high-level type synthesis algorithm *)
 
   let understand_gen kind sigma env c =
@@ -604,8 +616,15 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   let understand_ltac sigma env lvar kind c =
     ise_pretype_gen false sigma env lvar kind c
       
-  let understand_tcc_evars isevars env kind c =
-    pretype_gen isevars env ([],[]) kind c
+  let understand_tcc_evars evdref env kind c =
+    pretype_gen evdref env ([],[]) kind c 
+
+(*     evdref := nf_evar_defs !evdref; *)
+(*     let c = nf_evar (evars_of !evdref) c in *)
+(*     let evd = undefined_evars !evdref in *)
+(*     let evd = Typeclasses.resolve_typeclasses env (evars_of evd) !evdref in *)
+(*       evdref := evd; *)
+(*       nf_evar (evars_of evd) c       *)
 
   let understand_tcc sigma env ?expected_type:exptyp c =
     let ev, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index d5df9adc92..46a8bd203c 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -357,19 +357,31 @@ let print_message m =
 
 (* Solve an obligation using tactics, return the corresponding proof term *)
 let solve_by_tac evi t =
-  debug 2 (str "Solving goal using tactics: " ++ Evd.pr_evar_info evi);
   let id = id_of_string "H" in
-  try 
+  try
     Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl
     (fun _ _ -> ());
-    debug 2 (str "Started proof");
     Pfedit.by (tclCOMPLETE t);
-    let _,(const,_,_) = Pfedit.cook_proof () in 
+    let _,(const,_,_) = Pfedit.cook_proof () in
       Pfedit.delete_current_proof (); const.Entries.const_entry_body
-  with e -> 
+  with e ->
     Pfedit.delete_current_proof();
     raise Exit
 
+(* let apply_tac t goal = t goal *)
+
+(* let solve_by_tac evi t = *)
+(*   let ev = 1 in *)
+(*   let evm = Evd.add Evd.empty ev evi in *)
+(*   let goal = {it = evi; sigma = evm } in *)
+(*   let (res, valid) = apply_tac 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 proofterm *)
+(* 	else raise Exit *)
+(*     else raise Exit *)
+
 let rec string_of_list sep f = function
     [] -> ""
   | x :: [] -> f x