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

25 files changed, 542 insertions, 216 deletions

diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index 8eeb8b642..56cea8e07 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -125,9 +125,9 @@ let mk_open_instance id gl m t=
   let rec raux n t=
     if n=0 then t else 
       match t with
-	  RLambda(loc,name,_,t0)->
+	  RLambda(loc,name,k,_,t0)->
 	    let t1=raux (n-1) t0 in
-	      RLambda(loc,name,RHole (dummy_loc,Evd.BinderType name),t1)
+	      RLambda(loc,name,k,RHole (dummy_loc,Evd.BinderType name),t1)
 	| _-> anomaly "can't happen" in
   let ntt=try 
     Pretyping.Default.understand evmap env (raux m rawt)
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 612be05e3..97f7c1d97 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -139,8 +139,8 @@ type newfixpoint_expr =
 let rec abstract_rawconstr c = function
   | [] -> c
   | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_rawconstr c bl)
-  | Topconstr.LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> Topconstr.mkLambdaC([x],t,b)) idl
+  | Topconstr.LocalRawAssum (idl,k,t)::bl ->
+      List.fold_right (fun x b -> Topconstr.mkLambdaC([x],k,t,b)) idl
         (abstract_rawconstr c bl)
 
 let interp_casted_constr_with_implicits sigma env impls c  =
@@ -213,7 +213,7 @@ let rec is_rec names =
     | RRec _ -> error "RRec not handled"
     | RIf(_,b,_,lhs,rhs) -> 
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
-    | RLetIn(_,na,t,b) | RLambda(_,na,t,b) | RProd(_,na,t,b)  -> 
+    | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b)  -> 
 	lookup names t || lookup (Nameops.name_fold Idset.remove na names) b
     | RLetTuple(_,nal,_,t,b) -> lookup names t || 
 	lookup 
@@ -434,7 +434,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
       | None -> 
 	  begin
 	    match args with 
-	      | [Topconstr.LocalRawAssum ([(_,Name x)],t)] -> t,x 
+	      | [Topconstr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x 
 	      | _ -> error "Recursive argument must be specified" 
 	  end
       | Some wf_args -> 
@@ -442,7 +442,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
 	    match 
 	      List.find 
 		(function 
-		   | Topconstr.LocalRawAssum(l,t) -> 
+		   | Topconstr.LocalRawAssum(l,k,t) -> 
 		       List.exists 
 			 (function (_,Name id) -> id =  wf_args | _ -> false) 
 			 l 
@@ -450,7 +450,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
 		)
 		args 
 	    with 
-	      | Topconstr.LocalRawAssum(_,t)  ->	    t,wf_args
+	      | Topconstr.LocalRawAssum(_,k,t)  ->	    t,wf_args
 	      | _ -> assert false 
 	  with Not_found -> assert false 
   in
@@ -462,7 +462,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b
   let fun_from_mes = 
     let applied_mes = 
       Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg])    in
-    Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],wf_arg_type,applied_mes) 
+    Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],Topconstr.default_binder_kind,wf_arg_type,applied_mes) 
   in
   let wf_rel_from_mes = 
     Topconstr.mkAppC(Topconstr.mkRefC  ltof,[wf_arg_type;fun_from_mes])
@@ -570,11 +570,11 @@ let rec add_args id new_args b =
       CArrow(loc,add_args id new_args  b1, add_args id new_args b2)
   | CProdN(loc,nal,b1) -> 
       CProdN(loc,
-	     List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal, 
+	     List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, 
 	     add_args id new_args  b1)
   | CLambdaN(loc,nal,b1) -> 
       CLambdaN(loc,
-	       List.map (fun (nal,b2) -> (nal,add_args id new_args  b2)) nal, 
+	       List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args  b2)) nal, 
 	       add_args id new_args  b1)
   | CLetIn(loc,na,b1,b2) -> 
       CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
@@ -644,13 +644,15 @@ let rec chop_n_arrow n t =
 	      let new_n =
 		let rec aux (n:int) = function 
 		    [] -> n
-		| (nal,t'')::nal_ta' -> 
+		| (nal,k,t'')::nal_ta' -> 
 		    let nal_l = List.length nal in 
 		    if n >= nal_l
 		    then 
 		      aux (n - nal_l) nal_ta'
 		    else 
-		      let new_t' = Topconstr.CProdN(dummy_loc,((snd (list_chop n nal)),t'')::nal_ta',t')
+		      let new_t' = 
+			Topconstr.CProdN(dummy_loc,
+					((snd (list_chop n nal)),k,t'')::nal_ta',t')
 		      in 
 		      raise (Stop new_t')
 		in
@@ -668,12 +670,12 @@ let rec get_args b t : Topconstr.local_binder list *
     | Topconstr.CLambdaN (loc, (nal_ta), b') -> 
 	begin
 	  let n = 
-	    (List.fold_left (fun n (nal,_) -> 
+	    (List.fold_left (fun n (nal,_,_) -> 
 			       n+List.length nal) 0 nal_ta )
 	  in
 	  let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in 
-	  (List.map (fun (nal,ta) -> 
-		       (Topconstr.LocalRawAssum (nal,ta))) nal_ta)@nal_tas, b'',t'' 
+	  (List.map (fun (nal,k,ta) -> 
+		       (Topconstr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' 
 	end
     | _ -> [],b,t
 
@@ -716,7 +718,7 @@ let make_graph (f_ref:global_reference) =
 			   (List.map 
 			      (function 
 				 | Topconstr.LocalRawDef (na,_)-> []
-				 | Topconstr.LocalRawAssum (nal,_) -> nal
+				 | Topconstr.LocalRawAssum (nal,_,_) -> nal
 			      )
 			      bl
 			   )
@@ -730,7 +732,7 @@ let make_graph (f_ref:global_reference) =
 			   (List.map 
 			      (function
  				 | Topconstr.LocalRawDef (na,_)-> []
-			      	 | Topconstr.LocalRawAssum (nal,_) -> 
+			      	 | Topconstr.LocalRawAssum (nal,_,_) -> 
 				     List.map 
 				       (fun (loc,n) -> 
 					  CRef(Libnames.Ident(loc, Nameops.out_name n))) 
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 5ad4632e4..78e2c4408 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -76,7 +76,7 @@ let chop_rlambda_n  =
       then List.rev acc,rt
       else
 	match rt with
-	  | Rawterm.RLambda(_,name,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
+	  | Rawterm.RLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
 	  | Rawterm.RLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
 	  | _ -> 
 	      raise (Util.UserError("chop_rlambda_n",
@@ -90,7 +90,7 @@ let chop_rprod_n  =
       then List.rev acc,rt
       else
 	match rt with
-	  | Rawterm.RProd(_,name,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
+	  | Rawterm.RProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
 	  | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
   in
   chop_prod_n []
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index b6398a329..4b3492b12 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -148,7 +148,7 @@ END
 VERNAC ARGUMENT EXTEND binder2
     [ "(" ne_ident_list(idl) ":" lconstr(c)  ")"] ->
      [
-       LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,c) ]
+       LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,Topconstr.default_binder_kind,c) ]
 END
 
 
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index 44df08598..adec67e36 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -830,7 +830,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
         let _ = prNamedRConstr (string_of_name nme) tp in
         let _ = prstr "  ;  " in
         let typ = rawterm_to_constr_expr tp in
-        LocalRawAssum ([(dummy_loc,nme)] , typ) :: acc)
+        LocalRawAssum ([(dummy_loc,nme)], Topconstr.default_binder_kind, typ) :: acc)
       [] params in
   let concl = Constrextern.extern_constr false (Global.env()) concl in
   let arity,_ = 
@@ -838,7 +838,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
       (fun (acc,env) (nm,_,c) -> 
         let typ = Constrextern.extern_constr false env c in
         let newenv = Environ.push_rel (nm,None,c) env in
-        CProdN (dummy_loc, [[(dummy_loc,nm)],typ] , acc) , newenv)
+        CProdN (dummy_loc, [[(dummy_loc,nm)],Topconstr.default_binder_kind,typ] , acc) , newenv)
       (concl,Global.env())
       (shift.funresprms2 @ shift.funresprms1 
         @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in  
@@ -867,7 +867,7 @@ let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) =
   match rdecl with
     | (nme,None,t) -> 
         let traw = Detyping.detype false [] [] t in
-        RProd (dummy_loc,nme,traw,t2)
+        RProd (dummy_loc,nme,Explicit,traw,t2)
     | (_,Some _,_) -> assert false
 
 
@@ -877,7 +877,7 @@ let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) =
   match rdecl with
     | (nme,None,t) -> 
         let traw = Detyping.detype false [] [] t in
-        RProd (dummy_loc,nme,traw,t2)
+        RProd (dummy_loc,nme,Explicit,traw,t2)
     | (_,Some _,_) -> assert false
 
 
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 2f6f5914d..9bea4f1e0 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -586,7 +586,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 	    | RProd _ -> error "Cannot apply a type"
 	end (* end of the application treatement *) 
 
-    | RLambda(_,n,t,b) ->
+    | RLambda(_,n,_,t,b) ->
 	(* we first compute the list of constructor 
 	   corresponding to the body of the function, 
 	   then the one corresponding to the type 
@@ -601,7 +601,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 	let new_env = raw_push_named (new_n,None,t) env in
 	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_lam new_n) t_res b_res
-    | RProd(_,n,t,b) ->
+    | RProd(_,n,_,t,b) ->
 	(* we first compute the list of constructor 
 	   corresponding to the body of the function, 
 	   then the one corresponding to the type 
@@ -865,7 +865,7 @@ let is_res id =
 *)
 let rec rebuild_cons nb_args relname args crossed_types depth rt = 
   match rt with 
-    | RProd(_,n,t,b) -> 
+    | RProd(_,n,k,t,b) -> 
 	let not_free_in_t id = not (is_free_in id t) in 
 	let new_crossed_types = t::crossed_types in 
 	begin
@@ -928,7 +928,7 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
 			(Idset.filter not_free_in_t id_to_exclude)
 		  | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
 	end
-    | RLambda(_,n,t,b) ->
+    | RLambda(_,n,k,t,b) ->
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let new_crossed_types = t :: crossed_types in
@@ -944,7 +944,7 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt =
 		then 
 		  new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
 		else
-		  RProd(dummy_loc,n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+		  RProd(dummy_loc,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude
 	    | _ -> anomaly "Should not have an anonymous function here" 
 		(* We have renamed all the anonymous functions during alpha_renaming phase *)
 	  
@@ -1016,7 +1016,7 @@ let rec compute_cst_params relnames params = function
       compute_cst_params_from_app [] (params,rtl)
   | RApp(_,f,args) -> 
       List.fold_left (compute_cst_params relnames) params (f::args)
-  | RLambda(_,_,t,b) | RProd(_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) -> 
+  | RLambda(_,_,_,t,b) | RProd(_,_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) -> 
       let t_params = compute_cst_params relnames params t in 
       compute_cst_params relnames t_params b
   | RCases _ -> params  (* If there is still cases at this point they can only be 
@@ -1153,7 +1153,7 @@ let do_build_inductive
 	 else
 	   Topconstr.CProdN
 	   (dummy_loc,
-	    [[(dummy_loc,n)],Constrextern.extern_rawconstr Idset.empty t],
+	   [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_rawconstr Idset.empty t],
 	    acc
 	   )
       )
@@ -1173,7 +1173,7 @@ let do_build_inductive
 	   Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_rawconstr Idset.empty t)
 	 else
 	 Topconstr.LocalRawAssum 
-	   ([(dummy_loc,n)], Constrextern.extern_rawconstr Idset.empty t)
+	   ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_rawconstr Idset.empty t)
       )
       rels_params
   in 
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index e8cce47ad..0c03c1e61 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -12,8 +12,8 @@ let idmap_is_empty m = m = Idmap.empty
 let mkRRef ref = RRef(dummy_loc,ref)
 let mkRVar id = RVar(dummy_loc,id)
 let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl)
-let mkRLambda(n,t,b) = RLambda(dummy_loc,n,t,b)
-let mkRProd(n,t,b) = RProd(dummy_loc,n,t,b)
+let mkRLambda(n,t,b) = RLambda(dummy_loc,n,Explicit,t,b)
+let mkRProd(n,t,b) = RProd(dummy_loc,n,Explicit,t,b)
 let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
 let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
 let mkRSort s = RSort(dummy_loc,s)
@@ -26,7 +26,7 @@ let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
 *)
 let raw_decompose_prod = 
   let rec raw_decompose_prod args = function 
-  | RProd(_,n,t,b) -> 
+  | RProd(_,n,k,t,b) -> 
       raw_decompose_prod ((n,t)::args) b 
   | rt -> args,rt
   in
@@ -34,7 +34,7 @@ let raw_decompose_prod =
 
 let raw_decompose_prod_or_letin = 
   let rec raw_decompose_prod args = function 
-  | RProd(_,n,t,b) -> 
+  | RProd(_,n,k,t,b) -> 
       raw_decompose_prod ((n,None,Some t)::args) b 
   | RLetIn(_,n,t,b) -> 
       raw_decompose_prod ((n,Some t,None)::args) b 
@@ -58,7 +58,7 @@ let raw_decompose_prod_n n =
     if i<=0 then args,c
     else
       match c with
-	| RProd(_,n,t,b) -> 
+	| RProd(_,n,_,t,b) -> 
 	    raw_decompose_prod (i-1) ((n,t)::args) b 
 	| rt -> args,rt
   in
@@ -70,7 +70,7 @@ let raw_decompose_prod_or_letin_n n =
     if i<=0 then args,c
     else
       match c with
-	| RProd(_,n,t,b) -> 
+	| RProd(_,n,_,t,b) -> 
 	    raw_decompose_prod (i-1) ((n,None,Some t)::args) b 
 	| RLetIn(_,n,t,b) -> 
 	    raw_decompose_prod (i-1) ((n,Some t,None)::args) b 
@@ -135,15 +135,17 @@ let change_vars =
 	       change_vars mapping rt',
 	       List.map (change_vars mapping) rtl
 	      )
-      | RLambda(loc,name,t,b) -> 
+      | RLambda(loc,name,k,t,b) -> 
 	  RLambda(loc,
 		  name,
+		  k,
 		  change_vars mapping t,
 		  change_vars (remove_name_from_mapping mapping name) b
 		 )
-      | RProd(loc,name,t,b) -> 
+      | RProd(loc,name,k,t,b) -> 
 	  RProd(loc,
 		  name,
+	          k,
 		  change_vars mapping t,
 		  change_vars (remove_name_from_mapping mapping name) b
 		 )
@@ -261,21 +263,21 @@ let rec alpha_rt excluded rt =
   let new_rt = 
     match rt with   
       | RRef _ | RVar _ | REvar _ | RPatVar _ -> rt
-      | RLambda(loc,Anonymous,t,b) -> 
+      | RLambda(loc,Anonymous,k,t,b) -> 
 	  let new_id = Nameops.next_ident_away (id_of_string "_x") excluded in 
 	  let new_excluded = new_id :: excluded in 
 	  let new_t = alpha_rt new_excluded t in 
 	  let new_b = alpha_rt new_excluded b in 
-	  RLambda(loc,Name new_id,new_t,new_b)
-      | RProd(loc,Anonymous,t,b) -> 
+	  RLambda(loc,Name new_id,k,new_t,new_b)
+      | RProd(loc,Anonymous,k,t,b) -> 
 	let new_t = alpha_rt excluded t in 
 	let new_b = alpha_rt excluded b in 
-	RProd(loc,Anonymous,new_t,new_b)
+	RProd(loc,Anonymous,k,new_t,new_b)
     | RLetIn(loc,Anonymous,t,b) -> 
 	let new_t = alpha_rt excluded t in 
 	let new_b = alpha_rt excluded b in 
 	RLetIn(loc,Anonymous,new_t,new_b)
-    | RLambda(loc,Name id,t,b) -> 
+    | RLambda(loc,Name id,k,t,b) -> 
 	let new_id = Nameops.next_ident_away id excluded in 
 	let t,b = 
 	  if new_id = id 
@@ -287,8 +289,8 @@ let rec alpha_rt excluded rt =
 	let new_excluded = new_id::excluded in 
 	let new_t = alpha_rt new_excluded t in 
 	let new_b = alpha_rt new_excluded b in 
-	RLambda(loc,Name new_id,new_t,new_b)
-    | RProd(loc,Name id,t,b) -> 
+	RLambda(loc,Name new_id,k,new_t,new_b)
+    | RProd(loc,Name id,k,t,b) -> 
 	let new_id = Nameops.next_ident_away id excluded in 
 	let new_excluded = new_id::excluded in 
 	let t,b = 
@@ -300,7 +302,7 @@ let rec alpha_rt excluded rt =
 	in
 	let new_t = alpha_rt new_excluded t in 
 	let new_b = alpha_rt new_excluded b in 
-	RProd(loc,Name new_id,new_t,new_b)
+	RProd(loc,Name new_id,k,new_t,new_b)
     | RLetIn(loc,Name id,t,b) -> 
 	let new_id = Nameops.next_ident_away id excluded in 
 	let t,b = 
@@ -389,7 +391,7 @@ let is_free_in id =
     | REvar _ -> false
     | RPatVar _ -> false
     | RApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl)
-    | RLambda(_,n,t,b) | RProd(_,n,t,b) | RLetIn(_,n,t,b) ->
+    | RLambda(_,n,_,t,b) | RProd(_,n,_,t,b) | RLetIn(_,n,t,b) ->
 	let check_in_b =
 	  match n with
 	    | Name id' -> id_ord id' id <> 0
@@ -460,17 +462,19 @@ let replace_var_by_term x_id term =
 	       replace_var_by_pattern rt',
 	       List.map replace_var_by_pattern rtl
 	      )
-      | RLambda(_,Name id,_,_) when id_ord id x_id == 0 -> rt
-      | RLambda(loc,name,t,b) -> 
+      | RLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
+      | RLambda(loc,name,k,t,b) -> 
 	  RLambda(loc,
 		  name,
+		  k,
 		  replace_var_by_pattern t,
 		  replace_var_by_pattern b
 		 )
-      | RProd(_,Name id,_,_) when id_ord id x_id == 0 -> rt
-      | RProd(loc,name,t,b) -> 
+      | RProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
+      | RProd(loc,name,k,t,b) -> 
 	  RProd(loc,
 		  name,
+	          k,
 		  replace_var_by_pattern t,
 		  replace_var_by_pattern b
 		 )
@@ -590,8 +594,8 @@ let ids_of_rawterm c =
       | RVar (_,id) -> id::acc
       | RApp (loc,g,args) -> 
           ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc
-      | RLambda (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
-      | RProd (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
+      | RLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
+      | RProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
       | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
       | RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
       | RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc
@@ -622,15 +626,17 @@ let zeta_normalize =
 	       zeta_normalize_term rt',
 	       List.map zeta_normalize_term rtl
 	      )
-      | RLambda(loc,name,t,b) -> 
+      | RLambda(loc,name,k,t,b) -> 
 	  RLambda(loc,
 		  name,
+		  k,
 		  zeta_normalize_term t,
 		  zeta_normalize_term b
 		 )
-      | RProd(loc,name,t,b) -> 
+      | RProd(loc,name,k,t,b) -> 
 	  RProd(loc,
-		name, 		  
+		name, 		
+	        k,
 		zeta_normalize_term t,
 		zeta_normalize_term b
 		 )
@@ -691,8 +697,8 @@ let expand_as =
 	    with Not_found -> rt 
 	  end
       | RApp(loc,f,args) -> RApp(loc,expand_as map f,List.map (expand_as map) args)
-      | RLambda(loc,na,t,b) -> RLambda(loc,na,expand_as map t, expand_as map b)
-      | RProd(loc,na,t,b) -> RProd(loc,na,expand_as map t, expand_as map b)
+      | RLambda(loc,na,k,t,b) -> RLambda(loc,na,k,expand_as map t, expand_as map b)
+      | RProd(loc,na,k,t,b) -> RProd(loc,na,k,expand_as map t, expand_as map b)
       | RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b)
       | RLetTuple(loc,nal,(na,po),v,b) ->
 	  RLetTuple(loc,nal,(na,Option.map (expand_as map) po),
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index b0a34cfd1..172c7479c 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -28,7 +28,7 @@ let convert_env =
     let convert_binder env (na, b, c) =
       match b with 
        | Some b -> LocalRawDef ((dummy_loc,na), extern_constr true env b)
-       | None -> LocalRawAssum ([dummy_loc,na], extern_constr true env c) in
+       | None -> LocalRawAssum ([dummy_loc,na], default_binder_kind, extern_constr true env c) in
     let rec cvrec env = function
        [] -> []
      | b::rest -> (convert_binder env b)::(cvrec (push_rel b env) rest) in
@@ -140,8 +140,8 @@ let make_variable_ast name typ implicits =
     
 
 let make_definition_ast name c typ implicits =
-  VernacDefinition ((Global,false,Definition), (dummy_loc,name), DefineBody ([], None,
-    (constr_to_ast c), Some (constr_to_ast typ)),
+  VernacDefinition ((Global,false,Definition), (dummy_loc,name), 
+		   DefineBody ([], None, constr_to_ast c, Some (constr_to_ast typ)),
     (fun _ _ -> ()))
   ::(implicits_to_ast_list implicits);;
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 0e4f66072..05c227de0 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -312,7 +312,7 @@ let make_fix_struct (n,bl) =
 
 
 let rec xlate_binder = function
-    (l,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
+    (l,k,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
 and xlate_return_info = function
 | (Some Anonymous, None) | (None, None) ->
    CT_coerce_NONE_to_RETURN_INFO CT_none
@@ -325,7 +325,7 @@ and xlate_formula_opt =
     | Some e -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula e)
 
 and  xlate_binder_l = function
-    LocalRawAssum(l,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
+    LocalRawAssum(l,_,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
   | LocalRawDef(n,v) -> CT_coerce_DEF_to_BINDER(CT_def(xlate_id_opt n,
 						       xlate_formula v))
 and 
@@ -459,7 +459,7 @@ and xlate_matched_formula = function
       CT_coerce_FORMULA_to_MATCHED_FORMULA(xlate_formula f)
 and xlate_formula_expl = function
     (a, None) -> xlate_formula a
-  | (a, Some (_,ExplByPos i)) -> 
+  | (a, Some (_,ExplByPos (i, _))) -> 
       xlate_error "explicitation of implicit by rank not supported"
   | (a, Some (_,ExplByName i)) ->
       CT_labelled_arg(CT_ident (string_of_id i), xlate_formula a)
@@ -1609,7 +1609,7 @@ let rec xlate_vernac =
    | VernacDeclareTacticDefinition (true, tacs) ->
        (match List.map 
 	 (function
-	      ((_, id), body) ->
+	      ((_, id), _, body) ->
 		CT_tac_def(CT_ident (string_of_id id), xlate_tactic body))
 	 tacs with
 	     [] -> assert false
@@ -1834,6 +1834,10 @@ let rec xlate_vernac =
 	    xlate_error "TODO: Print Canonical Structures"
 	| PrintAssumptions _ -> 
 	    xlate_error "TODO: Print Needed Assumptions"
+	| PrintInstances _ -> 
+	    xlate_error "TODO: Print Instances"
+	| PrintTypeClasses -> 
+	    xlate_error "TODO: Print TypeClasses"
 	| PrintInspect n -> CT_inspect (CT_int n)
 	| PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s)
 	| PrintSetoids -> CT_print_setoids
@@ -2075,6 +2079,12 @@ let rec xlate_vernac =
        | Local -> CT_local in
       CT_coercion (local_opt, id_opt, xlate_ident id1,
         xlate_class id2, xlate_class id3)
+
+    (* TypeClasses *) 
+   | VernacSetInstantiationTactic _|VernacDeclareInstance _|VernacContext _|
+	 VernacInstance (_, _, _)|VernacClass (_, _, _, _, _) ->
+	   xlate_error "TODO: Type Classes commands"
+
   | VernacResetName id -> CT_reset (xlate_ident (snd id))
   | VernacResetInitial -> CT_restore_state (CT_ident "Initial")
   | VernacExtend (s, l) ->
@@ -2088,7 +2098,7 @@ let rec xlate_vernac =
   | VernacNop -> CT_proof_no_op
   | VernacComments l -> 
       CT_scomments(CT_scomment_content_list (List.map xlate_comment l))
-  | VernacDeclareImplicits(true, id, opt_positions) ->
+  | VernacDeclareImplicits(true, id, _, opt_positions) ->
       CT_implicits
 	(reference_to_ct_ID id,
 	 match opt_positions with
@@ -2097,11 +2107,11 @@ let rec xlate_vernac =
 	       CT_coerce_ID_LIST_to_ID_LIST_OPT
 	       (CT_id_list
 	       (List.map
-		  (function ExplByPos x, _
+		  (function ExplByPos (x,_), _, _
 		       -> xlate_error
 			   "explication argument by rank is obsolete"
-		     | ExplByName id, _ -> CT_ident (string_of_id id)) l)))
-  | VernacDeclareImplicits(false, id, opt_positions) ->
+		     | ExplByName id, _, _ -> CT_ident (string_of_id id)) l)))
+  | VernacDeclareImplicits(false, id, _, opt_positions) ->
       xlate_error "TODO: Implicit Arguments Global"
   | VernacReserve((_,a)::l, f) ->
       CT_reserve(CT_id_ne_list(xlate_ident a, 
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 26b6b3094..87c4d9bc7 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -1061,7 +1061,7 @@ let (value_f:constr list -> global_reference -> constr) =
       List.fold_left2 
 	(fun acc x_id a -> 
 	   RLambda
-      	     (d0, Name x_id, RDynamic(d0, constr_in a),
+      	     (d0, Name x_id, Explicit, RDynamic(d0, constr_in a),
 	      acc
 	     ) 
 	)
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index d1b4b50eb..9cb65f76e 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 a2582c5ca..e23fd535c 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 c2691c781..49e312aeb 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 4f5e302c2..56ebc4f52 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 34c398289..e46ca822e 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 000000000..da91b0406
--- /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 000000000..ce4b32cad
--- /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 a9a30c57a..9afa6f067 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 e3cf7a57a..c184169ac 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 cd70d5233..30fbd0284 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 a0e7e6951..0703bcb83 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 afe554c87..4af37043f 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 0ed0632c6..a2d5be66c 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 d5df9adc9..46a8bd203 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
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 82d7c19e5..3a0fdfb9b 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -491,7 +491,10 @@ let kind_of_constant kn =
     | DK.IsDefinition DK.IdentityCoercion ->
         Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) ->
+    | DK.IsDefinition DK.Instance ->
+        Pp.warning "Instance not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition" 
+   | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) ->
         "THEOREM",DK.string_of_theorem_kind thm
     | DK.IsProof _ ->
         Pp.warning "Unsupported theorem kind (used Theorem instead)";