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

12 files changed, 534 insertions, 49 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 058f3d210..e71083c50 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1408,9 +1408,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),_,_,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),_,_,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) 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 2cfa7076a..a9e550bf7 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -268,7 +268,7 @@ let is_nondep_branch c n =
 let extract_nondep_branches test c b n =
   let rec strip n r = if n=0 then r else
     match r with
-      | RLambda (_,_,_,t) -> strip (n-1) t
+      | RLambda (_,_,_,_,t) -> strip (n-1) t
       | RLetIn (_,_,_,t) -> strip (n-1) t
       | _ -> assert false in
   if test c n then Some (strip n b) else None
@@ -276,7 +276,7 @@ let extract_nondep_branches test c b n =
 let it_destRLambda_or_LetIn_names n c =
   let rec aux n nal c =
     if n=0 then (List.rev nal,c) else match c with
-      | RLambda (_,na,_,c) -> aux (n-1) (na::nal) c
+      | RLambda (_,na,_,_,c) -> aux (n-1) (na::nal) c
       | RLetIn (_,na,_,c) -> aux (n-1) (na::nal) c
       | _ ->
           (* eta-expansion *)
@@ -308,7 +308,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
         | Some p ->
             let nl,typ = it_destRLambda_or_LetIn_names k p in
 	    let n,typ = match typ with 
-              | RLambda (_,x,t,c) -> x, c
+              | RLambda (_,x,_,t,c) -> x, c
 	      | _ -> Anonymous, typ in
 	    let aliastyp =
 	      if List.for_all ((=) Anonymous) nl then None
@@ -444,14 +444,14 @@ and share_names isgoal n l avoid env c t =
         let t = detype isgoal avoid env t in
 	let id = next_name_away na avoid in 
         let avoid = id::avoid and env = add_name (Name id) env in
-        share_names isgoal (n-1) ((Name id,None,t)::l) avoid env c c'
+        share_names isgoal (n-1) ((Name id,Explicit,None,t)::l) avoid env c c'
     (* May occur for fix built interactively *)
     | LetIn (na,b,t',c), _ when n > 0 ->
         let t' = detype isgoal avoid env t' in
         let b = detype isgoal avoid env b in
 	let id = next_name_away na avoid in 
         let avoid = id::avoid and env = add_name (Name id) env in
-        share_names isgoal n ((Name id,Some b,t')::l) avoid env c t
+        share_names isgoal n ((Name id,Explicit,Some b,t')::l) avoid env c t
     (* Only if built with the f/n notation or w/o let-expansion in types *)
     | _, LetIn (_,b,_,t) when n > 0 ->
 	share_names isgoal n l avoid env c (subst1 b t)
@@ -461,7 +461,7 @@ and share_names isgoal n l avoid env c t =
 	let id = next_name_away na' avoid in 
         let avoid = id::avoid and env = add_name (Name id) env in
         let appc = mkApp (lift 1 c,[|mkRel 1|]) in
-        share_names isgoal (n-1) ((Name id,None,t')::l) avoid env appc c'
+        share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env appc c'
     (* If built with the f/n notation: we renounce to share names *)
     | _ ->
         if n>0 then warning "Detyping.detype: cannot factorize fix enough";
@@ -524,8 +524,8 @@ and detype_binder isgoal bk avoid env na ty c =
       concrete_name (avoid_flag isgoal) avoid env na c in
   let r =  detype isgoal avoid' (add_name na' env) c in
   match bk with
-  | BProd -> RProd (dl, na',detype isgoal avoid env ty, r)
-  | BLambda -> RLambda (dl, na',detype isgoal avoid env ty, r)
+  | BProd -> RProd (dl, na',Explicit,detype isgoal avoid env ty, r)
+  | BLambda -> RLambda (dl, na',Explicit,detype isgoal avoid env ty, r)
   | BLetIn -> RLetIn (dl, na',detype isgoal avoid env ty, r)
 
 let rec detype_rel_context where avoid env sign =
@@ -541,7 +541,7 @@ let rec detype_rel_context where avoid env sign =
 	    else concrete_name None avoid env na c in
       let b = Option.map (detype false avoid env) b in
       let t = detype false avoid env t in
-      (na',b,t) :: aux avoid' (add_name na' env) rest
+      (na',Explicit,b,t) :: aux avoid' (add_name na' env) rest
   in aux avoid env (List.rev sign)
 
 (**********************************************************************)
@@ -573,15 +573,15 @@ let rec subst_rawconstr subst raw =
 	if r' == r && rl' == rl then raw else
 	  RApp(loc,r',rl')
 
-  | RLambda (loc,n,r1,r2) -> 
+  | RLambda (loc,n,bk,r1,r2) -> 
       let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
-	  RLambda (loc,n,r1',r2')
+	  RLambda (loc,n,bk,r1',r2')
 
-  | RProd (loc,n,r1,r2) -> 
+  | RProd (loc,n,bk,r1,r2) -> 
       let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
-	  RProd (loc,n,r1',r2')
+	  RProd (loc,n,bk,r1',r2')
 
   | RLetIn (loc,n,r1,r2) -> 
       let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
@@ -629,10 +629,10 @@ let rec subst_rawconstr subst raw =
       let ra1' = array_smartmap (subst_rawconstr subst) ra1
       and ra2' = array_smartmap (subst_rawconstr subst) ra2 in
       let bl' = array_smartmap
-        (list_smartmap (fun (na,obd,ty as dcl) ->
+        (list_smartmap (fun (na,k,obd,ty as dcl) ->
           let ty' = subst_rawconstr subst ty in
           let obd' = Option.smartmap (subst_rawconstr subst) obd in
-          if ty'==ty & obd'==obd then dcl else (na,obd',ty')))
+          if ty'==ty & obd'==obd then dcl else (na,k,obd',ty')))
         bl in
 	if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
 	  RRec (loc,fix,ida,bl',ra1',ra2')
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 588bc8c84..72379dfcf 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -41,7 +41,7 @@ val detype_case :
 val detype_sort : sorts -> rawsort
 
 val detype_rel_context : constr option -> identifier list -> names_context ->
-  rel_context -> (name * rawconstr option * rawconstr) list
+  rel_context -> rawdecl list
 
 (* look for the index of a named var or a nondep var as it is renamed *)
 val lookup_name_as_renamed  : env -> constr -> identifier -> int option
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index b894a9aae..37d60e470 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -520,11 +520,11 @@ let build_mutual_indrec env sigma = function
     	(List.map
 	   (function (mind',mibi',mipi',dep',s') ->
 	      let (sp',_) = mind' in
-	      if sp=sp' then 
+	      if sp=sp' then
                 let (mibi',mipi') = lookup_mind_specif env mind' in
-		(mind',mibi',mipi',dep',s') 
-	      else 
-		raise (RecursionSchemeError (NotMutualInScheme (mind,mind'))))
+		(mind',mibi',mipi',dep',s')
+	      else
+		  raise (RecursionSchemeError (NotMutualInScheme (mind,mind'))))
 	   lrecspec)
       in
       let _ = check_arities listdepkind in 
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 63dfbb2d9..845f9fae1 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -220,10 +220,10 @@ let rec pat_of_raw metas vars = function
   | RApp (_,c,cl) -> 
       PApp (pat_of_raw metas vars c,
 	    Array.of_list (List.map (pat_of_raw metas vars) cl))
-  | RLambda (_,na,c1,c2) ->
+  | RLambda (_,na,bk,c1,c2) ->
       PLambda (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | RProd (_,na,c1,c2) ->
+  | RProd (_,na,bk,c1,c2) ->
       PProd (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
   | RLetIn (_,na,c1,c2) ->
@@ -241,7 +241,7 @@ let rec pat_of_raw metas vars = function
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
   | RLetTuple (loc,nal,(_,None),b,c) ->
-      let mkRLambda c na = RLambda (loc,na,RHole (loc,Evd.InternalHole),c) in
+      let mkRLambda c na = RLambda (loc,na,Explicit,RHole (loc,Evd.InternalHole),c) in
       let c = List.fold_left mkRLambda c nal in
       PCase ((LetStyle,[|1|],None,None),PMeta None,pat_of_raw metas vars b,
              [|pat_of_raw metas vars c|])
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9ecd7e251..3689ae174 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -321,11 +321,11 @@ module Pretyping_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,bk,None,ty)::bl ->
               let ty' = pretype_type empty_valcon env evdref 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,bk,Some bd,ty)::bl ->
               let ty' = pretype_type empty_valcon env evdref lvar ty in
               let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar ty in
               let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
@@ -420,7 +420,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  | _ -> resj in
 	inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-    | RLambda(loc,name,c1,c2)      ->
+    | RLambda(loc,name,bk,c1,c2)      ->
 	let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon in
 	let dom_valcon = valcon_of_tycon dom in
 	let j = pretype_type dom_valcon env evdref lvar c1 in
@@ -428,7 +428,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	let j' = pretype rng (push_rel var env) evdref lvar c2 in 
 	  judge_of_abstraction env (orelse_name name name') j j'
 
-    | RProd(loc,name,c1,c2)        ->
+    | RProd(loc,name,bk,c1,c2)        ->
 	let j = pretype_type empty_valcon env evdref lvar c1 in
 	let var = (name,j.utj_val) in
 	let env' = push_rel_assum var env in
@@ -652,7 +652,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	    (pretype tycon env evdref lvar c).uj_val
       | IsType ->
 	  (pretype_type empty_valcon env evdref lvar c).utj_val in
-      nf_evar (evars_of !evdref) c'
+    let evd,_ = consider_remaining_unif_problems env !evdref in
+    let evd = nf_evar_defs evd in
+    let c' = nf_evar (evars_of evd) c' in
+    let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in
+    let c' = nf_evar (evars_of evd) c' in
+      evdref := 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
@@ -680,10 +686,15 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let ise_pretype_gen fail_evar sigma env lvar kind c =
     let evdref = ref (Evd.create_evar_defs sigma) in
     let c = pretype_gen evdref env lvar kind c in
+(*     let evd,_ = consider_remaining_unif_problems env !evdref 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,_ = consider_remaining_unif_problems env !evdref in
-    let c = nf_evar (evars_of evd) c in
-    if fail_evar then check_evars env sigma evd c;
-    evd, c
+      if fail_evar then check_evars env (Evd.evars_of evd) evd c;
+      evd, c
 
   (** Entry points of the high-level type synthesis algorithm *)
 
@@ -701,6 +712,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       
   let understand_tcc_evars evdref env kind c =
     pretype_gen evdref env ([],[]) kind c
+(*     let c = pretype_gen evdref env ([],[]) kind c in *)
+(*     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 evd, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index d2a347363..bf5cc2272 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -36,6 +36,8 @@ type rawsort = RProp of Term.contents | RType of Univ.universe option
 
 type binder_kind = BProd | BLambda | BLetIn
 
+type binding_kind = Explicit | Implicit
+
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
 
 type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list
@@ -57,8 +59,8 @@ type rawconstr =
   | REvar of loc * existential_key * rawconstr list option
   | RPatVar of loc * (bool * patvar) (* Used for patterns only *)
   | RApp of loc * rawconstr * rawconstr list
-  | RLambda of loc * name * rawconstr * rawconstr
-  | RProd of loc * name * rawconstr * rawconstr
+  | RLambda of loc * name * binding_kind * rawconstr * rawconstr
+  | RProd of loc * name * binding_kind * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
   | RCases of loc * rawconstr option * tomatch_tuple * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
@@ -71,7 +73,7 @@ type rawconstr =
   | RCast of loc * rawconstr * rawconstr cast_type
   | RDynamic of loc * Dyn.t
 
-and rawdecl = name * rawconstr option * rawconstr
+and rawdecl = name * binding_kind * rawconstr option * rawconstr
 
 and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr
 
@@ -101,13 +103,13 @@ let cases_predicate_names tml =
 
    - boolean in POldCase means it is recursive
 i*)
-let map_rawdecl f (na,obd,ty) = (na,Option.map f obd,f ty)
+let map_rawdecl f (na,k,obd,ty) = (na,k,Option.map f obd,f ty)
 
 let map_rawconstr f = function
   | RVar (loc,id) -> RVar (loc,id)
   | RApp (loc,g,args) -> RApp (loc,f g, List.map f args)
-  | RLambda (loc,na,ty,c) -> RLambda (loc,na,f ty,f c)
-  | RProd (loc,na,ty,c) -> RProd (loc,na,f ty,f c)
+  | RLambda (loc,na,bk,ty,c) -> RLambda (loc,na,bk,f ty,f c)
+  | RProd (loc,na,bk,ty,c) -> RProd (loc,na,bk,f ty,f c)
   | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c)
   | RCases (loc,rtntypopt,tml,pl) ->
       RCases (loc,Option.map f rtntypopt,
@@ -166,8 +168,8 @@ let occur_rawconstr id =
   let rec occur = function
     | RVar (loc,id') -> id = id'
     | RApp (loc,f,args) -> (occur f) or (List.exists occur args)
-    | RLambda (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
-    | RProd (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
+    | RLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
+    | RProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c))
     | RCases (loc,rtntypopt,tml,pl) ->
 	(occur_option rtntypopt)
@@ -182,7 +184,7 @@ let occur_rawconstr id =
         not (array_for_all4 (fun fid bl ty bd ->
           let rec occur_fix = function
               [] -> not (occur ty) && (fid=id or not(occur bd))
-            | (na,bbd,bty)::bl ->
+            | (na,k,bbd,bty)::bl ->
                 not (occur bty) &&
                 (match bbd with
                     Some bd -> not (occur bd)
@@ -211,7 +213,7 @@ let free_rawvars  =
   let rec vars bounded vs = function
     | RVar (loc,id') -> if Idset.mem id' bounded then vs else Idset.add id' vs
     | RApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
-    | RLambda (loc,na,ty,c) | RProd (loc,na,ty,c) | RLetIn (loc,na,ty,c) -> 
+    | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) -> 
 	let vs' = vars bounded vs ty in 
 	let bounded' = add_name_to_ids bounded na in 
 	vars bounded' vs' c
@@ -234,7 +236,7 @@ let free_rawvars  =
 	let vars_fix i vs fid = 
 	  let vs1,bounded1 = 
 	    List.fold_left 
-	      (fun (vs,bounded) (na,bbd,bty) -> 
+	      (fun (vs,bounded) (na,k,bbd,bty) -> 
 		 let vs' = vars_option bounded vs bbd in 
 		 let vs'' = vars bounded vs' bty in
 		 let bounded' = add_name_to_ids bounded na in 
@@ -272,8 +274,8 @@ let loc_of_rawconstr = function
   | REvar (loc,_,_) -> loc
   | RPatVar (loc,_) -> loc
   | RApp (loc,_,_) -> loc
-  | RLambda (loc,_,_,_) -> loc
-  | RProd (loc,_,_,_) -> loc
+  | RLambda (loc,_,_,_,_) -> loc
+  | RProd (loc,_,_,_,_) -> loc
   | RLetIn (loc,_,_,_) -> loc
   | RCases (loc,_,_,_) -> loc
   | RLetTuple (loc,_,_,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index c43c290e8..2a5dab6e4 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -40,6 +40,8 @@ type rawsort = RProp of Term.contents | RType of Univ.universe option
 
 type binder_kind = BProd | BLambda | BLetIn
 
+type binding_kind = Explicit | Implicit
+
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
 
 type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list
@@ -61,8 +63,8 @@ type rawconstr =
   | REvar of loc * existential_key * rawconstr list option
   | RPatVar of loc * (bool * patvar) (* Used for patterns only *)
   | RApp of loc * rawconstr * rawconstr list
-  | RLambda of loc * name * rawconstr * rawconstr
-  | RProd of loc * name * rawconstr * rawconstr
+  | RLambda of loc * name * binding_kind *  rawconstr * rawconstr
+  | RProd of loc * name * binding_kind * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
   | RCases of loc * rawconstr option * tomatch_tuple * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
@@ -75,7 +77,7 @@ type rawconstr =
   | RCast of loc * rawconstr * rawconstr cast_type
   | RDynamic of loc * Dyn.t
 
-and rawdecl = name * rawconstr option * rawconstr
+and rawdecl = name * binding_kind * rawconstr option * rawconstr
 
 and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
new file mode 100644
index 000000000..b0e7cb147
--- /dev/null
+++ b/pretyping/typeclasses.ml
@@ -0,0 +1,311 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*)
+
+(*i*)
+open Names
+open Decl_kinds
+open Term
+open Sign
+open Evd
+open Environ
+open Nametab
+open Mod_subst
+open Util
+open Typeclasses_errors
+(*i*)
+
+let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
+(* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *)
+let mismatched_props env n m = mismatched_ctx_inst env Properties n m
+
+type rels = constr list
+
+(* This module defines type-classes *)
+type typeclass = {
+  cl_name : identifier; (* Name of the class *)
+  cl_context : named_context; (* Context in which superclasses and params are typed (usually types) *)
+  cl_super : named_context; (* Superclasses applied to some of the params *)
+  cl_params : named_context; (* Context of the parameters (usually types) *)
+(*   cl_defs : named_context; (\* Context of the definitions (usually functions), which may be shared *\) *)
+  cl_props : named_context; (* Context of the properties on defs, in Prop, will not be shared *)
+  cl_impl : inductive; (* The class implementation: a record parameterized by params and defs *)
+}
+
+type typeclasses = (identifier, typeclass) Gmap.t
+
+type instance = {
+  is_class: typeclass;
+  is_name: identifier; (* Name of the instance *)
+(*   is_params: named_context; (\* Context of the parameters, instanciated *\) *)
+(*   is_super: named_context; (\* The corresponding superclasses *\) *)
+(*   is_defs: named_context; (\* Context of the definitions, instanciated *\) *)
+  is_impl: constant; 
+(*   is_add_hint : unit -> unit; (\* Hook to add an hint for the instance *\) *)
+}
+
+type instances = (identifier, instance list) Gmap.t
+    
+let classes : typeclasses ref = ref Gmap.empty
+
+let methods : (identifier, identifier) Gmap.t ref = ref Gmap.empty
+  
+let instances : instances ref = ref Gmap.empty
+  
+let freeze () = !classes, !methods, !instances
+
+let unfreeze (cl,m,is) = 
+  classes:=cl;
+  methods:=m;
+  instances:=is
+    
+let init () =
+  classes:= Gmap.empty; 
+  methods:= Gmap.empty;
+  instances:= Gmap.empty
+    
+let _ = 
+  Summary.declare_summary "classes_and_instances"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
+      Summary.survive_module = true;
+      Summary.survive_section = true }
+
+let gmap_merge old ne =
+  Gmap.fold (fun k v acc -> Gmap.add k v acc) ne old
+
+let gmap_list_merge old ne =
+  let ne = 
+    Gmap.fold (fun k v acc -> 
+      let oldv = try Gmap.find k old with Not_found -> [] in
+      let v' = 
+	List.fold_left (fun acc x -> 
+	  if not (List.exists (fun y -> y.is_name = x.is_name) v) then x :: acc else acc)
+	v oldv
+      in Gmap.add k v' acc)
+      ne Gmap.empty
+  in
+    Gmap.fold (fun k v acc -> 
+      let newv = try Gmap.find k ne with Not_found -> [] in
+      let v' = 
+	List.fold_left (fun acc x -> 
+	  if not (List.exists (fun y -> y.is_name = x.is_name) acc) then x :: acc else acc)
+	  newv v
+      in Gmap.add k v' acc)
+      old ne
+
+let cache (_, (cl, m, inst)) =
+  classes := gmap_merge !classes cl;
+  methods := gmap_merge !methods m;
+  instances := gmap_list_merge !instances inst
+
+open Libobject
+
+let subst (_,subst,(cl,m,inst)) = 
+  let do_subst_con c = fst (Mod_subst.subst_con subst c)
+  and do_subst c = Mod_subst.subst_mps subst c
+  and do_subst_ind (kn,i) = (Mod_subst.subst_kn subst kn,i)
+  in
+  let do_subst_named ctx = 
+    List.map (fun (na, b, t) ->
+      (na, Option.smartmap do_subst b, do_subst t))
+      ctx
+  in
+  let subst_class cl = 
+    let cl' = { cl with cl_impl = do_subst_ind cl.cl_impl;
+		cl_context = do_subst_named cl.cl_context;
+		cl_super = do_subst_named cl.cl_super;
+		cl_params = do_subst_named cl.cl_params;
+		cl_props = do_subst_named cl.cl_props; }
+    in if cl' = cl then cl else cl'
+  in
+  let subst_inst classes insts =
+    List.map (fun is -> 
+      { is with is_class = Gmap.find is.is_class.cl_name classes; 
+	is_impl = do_subst_con is.is_impl }) insts
+  in
+  let classes = Gmap.map subst_class cl in
+  let instances = Gmap.map (subst_inst classes) inst in
+    (classes, m, instances)
+
+let discharge (_,(cl,m,inst)) =
+  let subst_class cl = 
+    { cl with cl_impl = Lib.discharge_inductive cl.cl_impl }
+  in
+  let subst_inst classes insts =
+    List.map (fun is -> { is with is_impl = Lib.discharge_con is.is_impl;
+      is_class = Gmap.find is.is_class.cl_name classes; }) insts
+  in
+  let classes = Gmap.map subst_class cl in
+  let instances = Gmap.map (subst_inst classes) inst in
+    Some (classes, m, instances)
+  
+let (input,output) = 
+  declare_object
+    { (default_object "type classes state") with
+      cache_function = cache;
+      load_function = (fun _ -> cache);
+      open_function = (fun _ -> cache);
+      classify_function = (fun (_,x) -> Substitute x);
+      discharge_function = discharge;
+      subst_function = subst;
+      export_function = (fun x -> Some x) }
+
+let update () = 
+  Lib.add_anonymous_leaf (input (!classes, !methods, !instances))
+
+let class_methods cl =
+  List.map (function (x, _, _) -> x) cl.cl_props
+
+let add_class c = 
+  classes := Gmap.add c.cl_name c !classes;
+  methods := List.fold_left (fun acc x -> Gmap.add x c.cl_name acc) !methods (class_methods c);
+  update ()
+    
+let class_info c = 
+  Gmap.find c !classes
+
+let class_of_inductive ind = 
+  let res = Gmap.fold 
+    (fun k v acc -> match acc with None -> if v.cl_impl = ind then Some v else acc | _ -> acc)
+    !classes None
+  in match res with
+      None -> raise Not_found
+    | Some cl -> cl
+
+let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes []
+
+let gmapl_add x y m =
+  try
+    let l = Gmap.find x m in
+    Gmap.add x (y::Util.list_except y l) m
+  with Not_found ->
+    Gmap.add x [y] m
+
+let instances_of c = 
+  try Gmap.find c.cl_name !instances with Not_found -> []
+
+let add_instance i =
+  instances := gmapl_add i.is_class.cl_name i !instances;
+  update ()
+
+open Libnames
+      
+let id_of_reference r = 
+  let (_, id) = repr_qualid (snd (qualid_of_reference r)) in id
+
+let instances r = 
+  let id = id_of_reference r in
+    try let cl = class_info id in instances_of cl
+    with Not_found -> unbound_class (Global.env()) (loc_of_reference r, id)
+
+let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false)
+
+let resolve_typeclass env ev evi (evd, defined as acc) =
+  if evi.evar_body = Evar_empty then
+    try
+      !solve_instanciation_problem env evd ev evi
+    with Exit -> acc
+  else acc
+
+let resolve_one_typeclass env types =
+  try
+    let evi = Evd.make_evar (Environ.named_context_val env) types in
+    let ev = 1 in
+    let evm = Evd.add Evd.empty ev evi in
+    let evd = Evd.create_evar_defs evm in
+    let evd', b = !solve_instanciation_problem env evd ev evi in
+      if b then 
+	let evm' = Evd.evars_of evd' in
+	  match Evd.evar_body (Evd.find evm' ev) with
+	      Evar_empty -> raise Not_found
+	    | Evar_defined c -> c
+      else raise Not_found
+  with Exit -> raise Not_found
+
+let resolve_one_typeclass_evd env evd types =
+  try
+    let ev = Evarutil.e_new_evar evd env types in
+    let (ev,_) = destEvar ev in
+    let evd', b =
+	!solve_instanciation_problem env !evd ev (Evd.find (Evd.evars_of !evd) ev)
+    in
+      evd := evd';
+      if b then 
+	let evm' = Evd.evars_of evd' in
+	  match Evd.evar_body (Evd.find evm' ev) with
+	      Evar_empty -> raise Not_found
+	    | Evar_defined c -> c
+      else raise Not_found
+  with Exit -> raise Not_found
+
+let method_typeclass ref = 
+  match ref with 
+    | ConstRef c -> 
+	let (_, _, l) = Names.repr_con c in
+	  class_info (Gmap.find (Names.id_of_label l) !methods)
+    | _ -> raise Not_found
+      
+let is_class ind = 
+  Gmap.fold (fun k v acc -> acc || v.cl_impl = ind) !classes false
+  
+let is_implicit_arg k = 
+  match k with
+      ImplicitArg (ref, (n, id)) -> true
+    | InternalHole -> true
+    | _ -> false
+
+let resolve_typeclasses ?(check=true) env sigma evd =
+  let evm = Evd.evars_of evd in
+  let tc_evars = 
+    let f ev evi acc =
+      let (l, k) = Evd.evar_source ev evd in
+	if not check || is_implicit_arg k then
+	  match kind_of_term evi.evar_concl with
+	    | App(ki, args) when isInd ki -> 
+		if is_class (destInd ki) then Evd.add acc ev evi
+		else acc
+	    | _ -> acc
+	else acc
+    in Evd.fold f evm Evd.empty
+  in
+  let rec sat evars =
+    let (evars', progress) = 
+      Evd.fold 
+	(fun ev evi acc -> 
+	  if Evd.mem tc_evars ev then resolve_typeclass env ev evi acc else acc) 
+	(Evd.evars_of evars) (evars, false) 
+    in
+      if not progress then evars'
+      else
+	sat (Evarutil.nf_evar_defs evars')
+  in sat evd
+
+let class_of_constr c = 
+  match kind_of_term c with
+      App (c, _) -> 
+	(match kind_of_term c with
+	    Ind ind -> (try Some (class_of_inductive ind) with Not_found -> None)
+	  | _ -> None)
+    | _ -> None
+
+
+type substitution = (identifier * constr) list
+
+let substitution_of_named_context isevars env id n subst l = 
+  List.fold_right
+    (fun (na, _, t) subst -> 
+      let t' = replace_vars subst t in
+      let b = Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (VarRef id, (n, Some na))) t' in
+	(na, b) :: subst)
+    l subst
+
+let nf_substitution sigma subst = 
+  List.map (function (na, c) -> na, Reductionops.nf_evar sigma c) subst
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
new file mode 100644
index 000000000..fbe48e06a
--- /dev/null
+++ b/pretyping/typeclasses.mli
@@ -0,0 +1,70 @@
+(************************************************************************)
+(*  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
+(*i*)
+
+(* This module defines type-classes *)
+type typeclass = {
+  cl_name : identifier; (* Name of the class *)
+  cl_context : named_context; (* Context in which superclasses and params are typed (usually types) *)
+  cl_super : named_context; (* Superclasses applied to some of the params *)
+  cl_params : named_context; (* Context of the real parameters (types and operations) *)
+(*   cl_defs : rel_context; (\* Context of the definitions (usually functions), which may be shared *\) *)
+  cl_props : named_context; (* Context of the properties on defs, in Prop, will not be shared *)
+  cl_impl : inductive; (* The class implementation: a record parameterized by params and defs *)
+}
+
+type instance = {
+  is_class: typeclass;
+  is_name: identifier; (* Name of the instance *)
+(*   is_params: named_context; (\* Context of the parameters, instanciated *\) *)
+(*   is_super: named_context; (\* The corresponding superclasses *\) *)
+  is_impl: constant; 
+(*   is_add_hint : unit -> unit; (\* Hook to add an hint for the instance *\) *)
+}
+  
+val instances : Libnames.reference -> instance list
+val typeclasses : unit -> typeclass list
+val add_class : typeclass -> unit
+val add_instance : instance -> unit
+
+val class_info : identifier -> typeclass (* raises Not_found *)
+val class_of_inductive : inductive -> typeclass (* raises Not_found *)
+
+val resolve_one_typeclass : env -> types -> types (* Raises Not_found *)
+val resolve_one_typeclass_evd : env -> evar_defs ref -> types -> types (* Raises Not_found *)
+
+val is_class : inductive -> bool
+
+val class_of_constr : constr -> typeclass option
+
+val resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_defs * bool
+val resolve_typeclasses : ?check:bool -> env -> evar_map -> evar_defs -> evar_defs
+
+val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref
+
+type substitution = (identifier * constr) list
+
+val substitution_of_named_context : 
+  evar_defs ref -> env -> identifier -> int ->
+  substitution -> named_context -> substitution
+
+val nf_substitution : evar_map -> substitution -> substitution
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
new file mode 100644
index 000000000..980f327cb
--- /dev/null
+++ b/pretyping/typeclasses_errors.ml
@@ -0,0 +1,42 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*)
+
+(*i*)
+open Names
+open Decl_kinds
+open Term
+open Sign
+open Evd
+open Environ
+open Nametab
+open Mod_subst
+open Topconstr
+open Util
+(*i*)
+
+type contexts = Parameters | Properties
+
+type typeclass_error = 
+    | UnboundClass of identifier located
+    | UnboundMethod of identifier * identifier located (* Class name, method *)
+    | NoInstance of identifier located * constr list
+    | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *)
+
+exception TypeClassError of env * typeclass_error
+
+let typeclass_error env err = raise (TypeClassError (env, err))
+
+let unbound_class env id = typeclass_error env (UnboundClass id)
+
+let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
+
+let no_instance env id args = typeclass_error env (NoInstance (id, args))
+
+let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
new file mode 100644
index 000000000..fbc2f2544
--- /dev/null
+++ b/pretyping/typeclasses_errors.mli
@@ -0,0 +1,40 @@
+(************************************************************************)
+(*  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
+(*i*)
+
+type contexts = Parameters | Properties
+
+type typeclass_error = 
+    | UnboundClass of identifier located
+    | UnboundMethod of identifier * identifier located (* Class name, method *)
+    | NoInstance of identifier located * constr list
+    | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *)
+
+exception TypeClassError of env * typeclass_error
+
+val unbound_class : env -> identifier located -> 'a
+
+val unbound_method : env -> identifier -> identifier located -> 'a
+
+val no_instance : env -> identifier located -> constr list -> 'a
+
+val mismatched_ctx_inst : env -> contexts -> constr_expr list -> named_context -> 'a