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

8 files changed, 428 insertions, 99 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 1117d25079..7e288f3117 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -216,7 +216,7 @@ let rec check_same_type ty1 ty2 =
   | _ when ty1=ty2 -> ()
   | _ -> failwith "not same type"
 
-and check_same_binder (nal1,e1) (nal2,e2) =
+and check_same_binder (nal1,_,e1) (nal2,_,e2) =
   List.iter2 (fun (_,na1) (_,na2) ->
     if na1<>na2 then failwith "not same name") nal1 nal2;
   check_same_type e1 e2
@@ -224,10 +224,10 @@ and check_same_binder (nal1,e1) (nal2,e2) =
 and check_same_fix_binder bl1 bl2 =
   List.iter2 (fun b1 b2 ->
     match b1,b2 with
-        LocalRawAssum(nal1,ty1), LocalRawAssum(nal2,ty2) ->
-          check_same_binder (nal1,ty1) (nal2,ty2)
+        LocalRawAssum(nal1,k,ty1), LocalRawAssum(nal2,k',ty2) ->
+          check_same_binder (nal1,k,ty1) (nal2,k',ty2)
       | LocalRawDef(na1,def1), LocalRawDef(na2,def2) ->
-          check_same_binder ([na1],def1) ([na2],def2)          
+          check_same_binder ([na1],default_binder_kind,def1) ([na2],default_binder_kind,def2)
       | _ -> failwith "not same binder") bl1 bl2
 
 let same c d = try check_same_type c d; true with _ -> false
@@ -255,10 +255,10 @@ let rec same_raw c d =
   | RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar"
   | RApp(_,f1,a1), RApp(_,f2,a2) ->
       List.iter2 same_raw (f1::a1) (f2::a2)
-  | RLambda(_,na1,t1,m1), RLambda(_,na2,t2,m2) ->
+  | RLambda(_,na1,bk1,t1,m1), RLambda(_,na2,bk2,t2,m2) ->
       if na1 <> na2 then failwith "RLambda";
       same_raw t1 t2; same_raw m1 m2
-  | RProd(_,na1,t1,m1), RProd(_,na2,t2,m2) ->
+  | RProd(_,na1,bk1,t1,m1), RProd(_,na2,bk2,t2,m2) ->
       if na1 <> na2 then failwith "RProd";
       same_raw t1 t2; same_raw m1 m2
   | RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) ->
@@ -283,7 +283,7 @@ let rec same_raw c d =
   | RRec(_,fk1,na1,bl1,ty1,def1), RRec(_,fk2,na2,bl2,ty2,def2) ->
       if fk1 <> fk2 || na1 <> na2 then failwith "RRec";
       array_iter2
-        (List.iter2 (fun (na1,bd1,ty1) (na2,bd2,ty2) ->
+        (List.iter2 (fun (na1,bk1,bd1,ty1) (na2,bk2,bd2,ty2) ->
           if na1<>na2 then failwith "RRec";
           Option.iter2 same_raw bd1 bd2;
           same_raw ty1 ty2)) bl1 bl2;
@@ -582,7 +582,7 @@ let rec rename_rawconstr_var id0 id1 = function
 
 let rec share_fix_binders n rbl ty def =
   match ty,def with
-      RProd(_,na0,t0,b), RLambda(_,na1,t1,m) ->
+      RProd(_,na0,bk0,t0,b), RLambda(_,na1,bk1,t1,m) ->
         if not(same_rawconstr t0 t1) then List.rev rbl, ty, def
         else
           let (na,b,m) =
@@ -672,7 +672,7 @@ let rec extern inctx scopes vars r =
 	     explicitize loc inctx [] (None,sub_extern false scopes vars f)
                (List.map (sub_extern true scopes vars) args))
 
-  | RProd (loc,Anonymous,t,c) ->
+  | RProd (loc,Anonymous,_,t,c) ->
       (* Anonymous product are never factorized *)
       CArrow (loc,extern_typ scopes vars t, extern_typ scopes vars c)
 
@@ -680,15 +680,15 @@ let rec extern inctx scopes vars r =
       CLetIn (loc,(loc,na),sub_extern false scopes vars t,
               extern inctx scopes (add_vname vars na) c)
 
-  | RProd (loc,na,t,c) ->
+  | RProd (loc,na,bk,t,c) ->
       let t = extern_typ scopes vars (anonymize_if_reserved na t) in
       let (idl,c) = factorize_prod scopes (add_vname vars na) t c in
-      CProdN (loc,[(dummy_loc,na)::idl,t],c)
+      CProdN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
 
-  | RLambda (loc,na,t,c) ->
+  | RLambda (loc,na,bk,t,c) ->
       let t = extern_typ scopes vars (anonymize_if_reserved na t) in
       let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
-      CLambdaN (loc,[(dummy_loc,na)::idl,t],c)
+      CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
 
   | RCases (loc,rtntypopt,tml,eqns) ->
       let vars' = 
@@ -775,7 +775,7 @@ and factorize_prod scopes vars aty c =
     if !Flags.raw_print or !print_no_symbol then raise No_match;
     ([],extern_symbol scopes vars c (uninterp_notations c))
   with No_match -> match c with
-  | RProd (loc,(Name id as na),ty,c)
+  | RProd (loc,(Name id as na),bk,ty,c)
       when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
 	& not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *)
 	-> let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in
@@ -787,7 +787,7 @@ and factorize_lambda inctx scopes vars aty c =
     if !Flags.raw_print or !print_no_symbol then raise No_match;
     ([],extern_symbol scopes vars c (uninterp_notations c))
   with No_match -> match c with
-  | RLambda (loc,na,ty,c)
+  | RLambda (loc,na,bk,ty,c)
       when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
 	& not (occur_name na aty) (* To avoid na in ty' escapes scope *)
 	-> let (nal,c) =
@@ -797,24 +797,24 @@ and factorize_lambda inctx scopes vars aty c =
 
 and extern_local_binder scopes vars = function
     [] -> ([],[])
-  | (na,Some bd,ty)::l ->
+  | (na,bk,Some bd,ty)::l ->
       let (ids,l) =
         extern_local_binder scopes (name_fold Idset.add na vars) l in
       (na::ids,
        LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l)
       
-  | (na,None,ty)::l ->
+  | (na,bk,None,ty)::l ->
       let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in
       (match extern_local_binder scopes (name_fold Idset.add na vars) l with
-          (ids,LocalRawAssum(nal,ty')::l)
+          (ids,LocalRawAssum(nal,k,ty')::l)
             when same ty ty' &
               match na with Name id -> not (occur_var_constr_expr id ty')
                 | _ -> true ->
               (na::ids,
-               LocalRawAssum((dummy_loc,na)::nal,ty')::l)
+               LocalRawAssum((dummy_loc,na)::nal,k,ty')::l)
         | (ids,l) ->
             (na::ids,
-             LocalRawAssum([(dummy_loc,na)],ty) :: l))
+             LocalRawAssum([(dummy_loc,na)],Default bk,ty) :: l))
 
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
   (loc,[List.map (extern_cases_pattern_in_scope scopes vars) pl],
@@ -927,11 +927,11 @@ let rec raw_of_pat env = function
       RApp (loc,RPatVar (loc,(true,n)),
         List.map (raw_of_pat env) args)
   | PProd (na,t,c) ->
-      RProd (loc,na,raw_of_pat env t,raw_of_pat (na::env) c)
+      RProd (loc,na,Explicit,raw_of_pat env t,raw_of_pat (na::env) c)
   | PLetIn (na,t,c) ->
       RLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
   | PLambda (na,t,c) ->
-      RLambda (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
+      RLambda (loc,na,Explicit,raw_of_pat env t, raw_of_pat (na::env) c)
   | PIf (c,b1,b2) ->
       RIf (loc, raw_of_pat env c, (Anonymous,None), 
            raw_of_pat env b1, raw_of_pat env b2)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a418253462..3214ca6c45 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -86,7 +86,7 @@ let explain_bad_patterns_number n1 n2 =
 
 let explain_bad_explicitation_number n po =
   match n with
-  | ExplByPos n ->
+  | ExplByPos (n,_id) ->
       let s = match po with
 	| None -> str "a regular argument"
 	| Some p -> int p in
@@ -683,7 +683,7 @@ let extract_explicit_arg imps args =
 		user_err_loc (loc,"",str "Argument name " ++ pr_id id
 		++ str " occurs more than once");
 	      id
-	  | ExplByPos p ->
+	  | ExplByPos (p,_id) ->
 	      let id =
 		try 
 		  let imp = List.nth imps (p-1) in
@@ -775,6 +775,16 @@ let set_type_scope (ids,tmp_scope,scopes) =
 let reset_tmp_scope (ids,tmp_scope,scopes) =
   (ids,None,scopes)
 
+let rec it_mkRProd env body =
+  match env with
+      (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body))
+    | [] -> body
+
+let rec it_mkRLambda env body =
+  match env with
+      (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body))
+    | [] -> body
+
 (**********************************************************************)
 (* Main loop                                                          *)
 
@@ -844,15 +854,15 @@ let internalise sigma globalenv env allow_patvar lvar c =
               Array.map (fun (_,ty,_) -> ty) idl,
               Array.map (fun (_,_,bd) -> bd) idl)
     | CArrow (loc,c1,c2) ->
-        RProd (loc, Anonymous, intern_type env c1, intern_type env c2)
+        RProd (loc, Anonymous, Explicit, intern_type env c1, intern_type env c2)
     | CProdN (loc,[],c2) ->
         intern_type env c2
-    | CProdN (loc,(nal,ty)::bll,c2) ->
-        iterate_prod loc env ty (CProdN (loc, bll, c2)) nal
+    | CProdN (loc,(nal,bk,ty)::bll,c2) ->
+        iterate_prod loc env bk ty (CProdN (loc, bll, c2)) nal
     | CLambdaN (loc,[],c2) ->
         intern env c2
-    | CLambdaN (loc,(nal,ty)::bll,c2) ->
-	iterate_lam loc (reset_tmp_scope env) ty (CLambdaN (loc, bll, c2)) nal
+    | CLambdaN (loc,(nal,bk,ty)::bll,c2) ->
+	iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal
     | CLetIn (loc,(_,na),c1,c2) ->
 	RLetIn (loc, na, intern (reset_tmp_scope env) c1,
           intern (push_name_env lvar env na) c2)
@@ -934,17 +944,20 @@ let internalise sigma globalenv env allow_patvar lvar c =
   and intern_type env = intern (set_type_scope env)
 
   and intern_local_binder ((ids,ts,sc as env),bl) = function
-    | LocalRawAssum(nal,ty) ->
-	let (loc,na) = List.hd nal in
-	(* TODO: fail if several names with different implicit types *)
-	let ty = locate_if_isevar loc na (intern_type env ty) in
-        List.fold_left
-          (fun ((ids,ts,sc),bl) (_,na) ->
-            ((name_fold Idset.add na ids,ts,sc), (na,None,ty)::bl))
-          (env,bl) nal
+    | LocalRawAssum(nal,bk,ty) ->
+	(match bk with
+	  | Default k ->
+	      let (loc,na) = List.hd nal in
+		(* TODO: fail if several names with different implicit types *)
+	      let ty = locate_if_isevar loc na (intern_type env ty) in
+		List.fold_left
+		  (fun ((ids,ts,sc),bl) (_,na) ->
+		    ((name_fold Idset.add na ids,ts,sc), (na,k,None,ty)::bl))
+		  (env,bl) nal
+	  | TypeClass b -> anomaly ("TODO: intern_local_binder TypeClass"))
     | LocalRawDef((loc,na),def) ->
         ((name_fold Idset.add na ids,ts,sc),
-         (na,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
+         (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
 
   (* Expands a multiple pattern into a disjunction of multiple patterns *)
   and intern_multiple_pattern scopes pl =
@@ -1004,22 +1017,50 @@ let internalise sigma globalenv env allow_patvar lvar c =
       | _, None -> Anonymous
       | _, Some na -> na in
     (tm',(na,typ)), na::ids
+      
+  and intern_typeclass_binders env bl =
+    List.fold_left 
+      (fun ((ids,ts,sc) as env,bl) ((loc, na), bk, ty) ->
+	let ty = locate_if_isevar loc na (intern_type env ty) in
+	  ((name_fold Idset.add na ids,ts,sc), (na,bk,None,ty)::bl))
+      env bl
 
-  and iterate_prod loc2 env ty body = function
+  and iterate_prod loc2 env bk ty body nal =
+    let rec default env bk = function
     | (loc1,na)::nal ->
 	if nal <> [] then check_capture loc1 ty na;
-	let body = iterate_prod loc2 (push_name_env lvar env na) ty body nal in
+	let body = default (push_name_env lvar env na) bk nal in
 	let ty = locate_if_isevar loc1 na (intern_type env ty) in
-	RProd (join_loc loc1 loc2, na, ty, body)
+	  RProd (join_loc loc1 loc2, na, bk, ty, body)
     | [] -> intern_type env body
-
-  and iterate_lam loc2 env ty body = function
-    | (loc1,na)::nal ->
-	if nal <> [] then check_capture loc1 ty na;
-	let body = iterate_lam loc2 (push_name_env lvar env na) ty body nal in
-	let ty = locate_if_isevar loc1 na (intern_type env ty) in
-	RLambda (join_loc loc1 loc2, na, ty, body)
-    | [] -> intern env body
+    in
+      match bk with
+	| Default b -> default env b nal
+	| TypeClass b -> 
+	    let ctx = (List.hd nal, b, ty) in
+	    let (fvs, bind) = Implicit_quantifiers.generalize_class_binders_raw (pi1 env) [ctx] in
+	    let env, ifvs = intern_typeclass_binders (env,[]) fvs in
+	    let env, ibind = intern_typeclass_binders (env,ifvs) bind in
+	    let body = intern_type env body in
+	      it_mkRProd ibind body
+					   
+  and iterate_lam loc2 env bk ty body nal = 
+    let rec default env bk = function 
+      | (loc1,na)::nal ->
+	  if nal <> [] then check_capture loc1 ty na;
+	  let body = default (push_name_env lvar env na) bk nal in
+	  let ty = locate_if_isevar loc1 na (intern_type env ty) in
+	    RLambda (join_loc loc1 loc2, na, bk, ty, body)
+      | [] -> intern env body
+    in match bk with
+      | Default b -> default env b nal
+      | TypeClass b ->
+	  let ctx = (List.hd nal, b, ty) in
+	  let (fvs, bind) = Implicit_quantifiers.generalize_class_binders_raw (pi1 env) [ctx] in
+	  let env, ifvs = intern_typeclass_binders (env,[]) fvs in
+	  let env, ibind = intern_typeclass_binders (env,ifvs) bind in
+	  let body = intern env body in
+	    it_mkRLambda ibind body
 
   and intern_impargs c env l subscopes args =
     let eargs, rargs = extract_explicit_arg l args in
@@ -1046,7 +1087,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
       | (imp::impl', []) -> 
 	  if eargs <> [] then 
 	    (let (id,(loc,_)) = List.hd eargs in
-	    user_err_loc (loc,"",str "Not enough non implicit
+	       user_err_loc (loc,"",str "Not enough non implicit
 	    arguments to accept the argument bound to " ++ pr_id id));
 	  []
       | ([], rargs) ->
@@ -1123,7 +1164,6 @@ let interp_open_constr sigma env c =
 let interp_constr_judgment sigma env c =
   Default.understand_judgment sigma env (intern_constr sigma env c)
 
-
 let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
   Default.understand_tcc_evars evdref env kind
     (intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c)
@@ -1175,11 +1215,11 @@ open Term
 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
@@ -1193,11 +1233,11 @@ let interp_context sigma env params =
 let interp_context_evars evdref 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_evars evdref 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_evars evdref 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
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index eac01a92ae..f4272a2b19 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -103,6 +103,8 @@ val interp_reference : ltac_sign -> reference -> rawconstr
 
 val interp_binder  : evar_map -> env -> name -> constr_expr -> types
 
+val interp_binder_evars : evar_defs ref -> env -> name -> constr_expr -> types
+
 (* Interpret contexts: returns extended env and context *)
 
 val interp_context : evar_map -> env -> local_binder list -> env * rel_context
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
new file mode 100644
index 0000000000..d9113644cb
--- /dev/null
+++ b/interp/implicit_quantifiers.ml
@@ -0,0 +1,215 @@
+(************************************************************************)
+(*  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 Rawterm
+open Topconstr
+open Libnames
+open Typeclasses
+open Typeclasses_errors
+(*i*)
+
+(* Auxilliary functions for the inference of implicitly quantified variables. *)    
+
+let free_vars_of_constr_expr c ?(bound=Idset.empty) l = 
+  let found id bdvars l = if Idset.mem id bdvars then l else if List.mem id l then l else id :: l in
+  let rec aux bdvars l c = match c with
+    | CRef (Ident (_,id)) -> found id bdvars l
+    | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id))) :: _) when not (Idset.mem id bdvars) ->
+	fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
+    | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
+  in aux bound l c
+
+
+let locate_reference qid =
+  match Nametab.extended_locate qid with
+    | TrueGlobal ref -> ref
+    | SyntacticDef kn -> 
+	match Syntax_def.search_syntactic_definition dummy_loc kn with
+	  | Rawterm.RRef (_,ref) -> ref
+	  | _ -> raise Not_found
+
+let is_global id =
+  try 
+    let _ = locate_reference (make_short_qualid id) in true
+  with Not_found -> 
+    false
+
+let is_freevar ids env x =
+  try
+    if Idset.mem x ids then false
+    else
+      try ignore(Environ.lookup_named x env) ; false
+      with _ -> not (is_global x)
+  with _ -> true
+
+let freevars_of_ids env ids = 
+  List.filter (is_freevar env (Global.env())) ids
+
+let compute_constrs_freevars env constrs =
+  let ids = 
+    List.rev (List.fold_left 
+		 (fun acc x -> free_vars_of_constr_expr x acc) 
+		 [] constrs)
+  in freevars_of_ids env ids
+
+(* let compute_context_freevars env ctx = *)
+(*   let ids = *)
+(*     List.rev *)
+(*       (List.fold_left *)
+(* 	  (fun acc (_,i,x) -> free_vars_of_constr_expr x acc) *)
+(* 	  [] constrs) *)
+(*   in freevars_of_ids ids *)
+
+let compute_constrs_freevars_binders env constrs =
+  let elts = compute_constrs_freevars env constrs in
+    List.map (fun id -> (dummy_loc, id), CHole dummy_loc) elts
+      
+let ids_of_named_context_avoiding avoid l =
+  List.fold_left (fun (ids, avoid) id -> 
+    let id' = Nameops.next_ident_away_from id avoid in id' :: ids, id' :: avoid) 
+    ([], avoid) (Termops.ids_of_named_context l)
+    
+let combine_params avoid applied needed =
+  let rec aux ids app need =
+    match app, need with
+	[], need -> 
+	  let need', avoid = ids_of_named_context_avoiding avoid need in
+	    List.rev ids @ (List.map mkIdentC need'), avoid
+      | x :: app, _ :: need -> aux (x :: ids) app need    
+      | _ :: _, [] -> failwith "combine_params: overly applied typeclass"
+  in aux [] applied needed
+
+let compute_context_vars env l =
+  List.fold_left (fun l (iid, _, c) -> 
+    (match snd iid with Name i -> [i] | Anonymous -> []) @ free_vars_of_constr_expr c ~bound:env l)
+    [] l
+
+let destClassApp cl =
+  match cl with
+    | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l
+    | _ -> raise Not_found
+
+let full_class_binders env l = 
+  let avoid = compute_context_vars env l in
+  let l', avoid =
+    List.fold_left (fun (l', avoid) (iid, bk, cl as x) -> 
+      match bk with
+	  Explicit -> 
+	    let (id, l) = destClassApp cl in
+	      (try
+		  let c = class_info (snd id) in
+		  let args, avoid = combine_params avoid l (List.rev c.cl_context @ List.rev c.cl_super @ List.rev c.cl_params) in
+		    (iid, bk, CAppExpl (fst id, (None, Ident id), args)) :: l', avoid
+		with Not_found -> unbound_class (Global.env ()) id)
+	| Implicit -> (x :: l', avoid))
+      ([], avoid) l
+  in List.rev l'
+      
+let constr_expr_of_constraint (kind, id) l =
+  match kind with
+    | Explicit -> CAppExpl (fst id, (None, Ident id), l)
+    | Implicit -> CApp (fst id, (None, CRef (Ident id)),
+		       List.map (fun x -> x, None) l)
+
+(*    | CApp of loc * (proj_flag * constr_expr) *  *)
+(*         (constr_expr * explicitation located option) list *)
+
+
+let constrs_of_context l =
+  List.map (fun (_, id, l) -> constr_expr_of_constraint id l) l
+
+let compute_context_freevars env ctx =
+  let bound, ids = 
+    List.fold_left 
+      (fun (bound, acc) (oid, id, x) -> 
+	let bound = match snd oid with Name n -> Idset.add n bound | Anonymous -> bound in
+	  bound, free_vars_of_constr_expr x ~bound acc)
+      (env,[]) ctx
+  in freevars_of_ids env (List.rev ids)
+
+let resolve_class_binders env l = 
+  let ctx = full_class_binders env l in
+  let fv_ctx = 
+    let elts = compute_context_freevars env ctx in
+      List.map (fun id -> (dummy_loc, id), CHole dummy_loc) elts
+  in
+    fv_ctx, ctx
+
+let generalize_class_binders env l = 
+  let fv_ctx, cstrs = resolve_class_binders env l in
+    List.map (fun ((loc, id), t) -> LocalRawAssum ([loc, Name id], Default Implicit, t)) fv_ctx,
+  List.map (fun (iid, bk, c) -> LocalRawAssum ([iid], Default Implicit, c)) 
+    cstrs
+
+let generalize_class_binders_raw env l = 
+  let fv_ctx, cstrs = resolve_class_binders env l in
+    List.map (fun ((loc, id), t) -> ((loc, Name id), Implicit, t)) fv_ctx,
+  List.map (fun (iid, bk, c) -> (iid, Implicit, c)) cstrs
+
+let ctx_of_class_binders env l = 
+  let (x, y) = generalize_class_binders env l in x @ y
+	
+let implicits_of_binders l = 
+  let rec aux i l = 
+    match l with 
+	[] -> []
+      | hd :: tl -> 
+	  let res, reslen = 
+	    match hd with
+		LocalRawAssum (nal, Default Implicit, t) -> 
+		  list_map_i (fun i (_,id) ->
+		    let name =
+		      match id with
+			  Name id -> Some id
+			| Anonymous -> None
+		    in ExplByPos (i, name), (true, true))
+		    i nal, List.length nal
+	      | LocalRawAssum (nal, _, _) -> [], List.length nal
+	      | LocalRawDef _ -> [], 1
+	  in res @ (aux (i + reslen) tl)
+  in aux 1 l
+  
+let implicits_of_rawterm l = 
+  let rec aux i c = 
+    match c with
+	RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> 
+	  let rest = aux (succ i) b in
+	    if bk = Implicit then
+	      let name =
+		match na with
+		    Name id -> Some id
+		  | Anonymous -> None
+	      in
+		(ExplByPos (i, name), (true, true)) :: rest
+	    else rest
+      | RLetIn (loc, na, t, b) -> aux i b
+      | _ -> []
+  in aux 1 l
+
+let nf_named_context sigma ctx = 
+  Sign.map_named_context (Reductionops.nf_evar sigma) ctx
+
+let nf_rel_context sigma ctx = 
+  Sign.map_rel_context (Reductionops.nf_evar sigma) ctx
+    
+let nf_env sigma env = 
+  let nc' = nf_named_context sigma (Environ.named_context env) in
+  let rel' = nf_rel_context sigma (Environ.rel_context env) in
+    push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
new file mode 100644
index 0000000000..a61dbcadf5
--- /dev/null
+++ b/interp/implicit_quantifiers.mli
@@ -0,0 +1,51 @@
+(************************************************************************)
+(*  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 Rawterm
+open Topconstr
+open Util
+open Typeclasses
+(*i*)
+
+val destClassApp : constr_expr -> identifier located * constr_expr list
+
+val free_vars_of_constr_expr :     Topconstr.constr_expr ->
+    ?bound:Idset.t ->
+    Names.identifier list -> Names.identifier list
+
+val compute_constrs_freevars : Idset.t -> constr_expr list -> identifier list
+val compute_constrs_freevars_binders : Idset.t -> constr_expr list -> (identifier located * constr_expr) list
+val resolve_class_binders : Idset.t -> typeclass_context -> 
+  (identifier located * constr_expr) list * typeclass_context
+
+val full_class_binders : Idset.t -> typeclass_context -> typeclass_context
+  
+val generalize_class_binders_raw : Idset.t -> typeclass_context -> 
+  (name located * binding_kind * constr_expr) list * (name located * binding_kind * constr_expr) list
+
+val ctx_of_class_binders : Idset.t -> typeclass_context -> local_binder list
+
+val implicits_of_binders : local_binder list -> (Topconstr.explicitation * (bool * bool)) list
+
+val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
+
+val nf_named_context : evar_map -> named_context -> named_context
+val nf_rel_context : evar_map -> rel_context -> rel_context
+val nf_env : evar_map -> env -> env
+
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 02e15f0690..f3c3506b5c 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -54,8 +54,8 @@ open Rawterm
 let rec unloc = function
   | RVar (_,id) -> RVar (dummy_loc,id)
   | RApp (_,g,args) -> RApp (dummy_loc,unloc g, List.map unloc args)
-  | RLambda (_,na,ty,c) -> RLambda (dummy_loc,na,unloc ty,unloc c)
-  | RProd (_,na,ty,c) -> RProd (dummy_loc,na,unloc ty,unloc c)
+  | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c)
+  | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c)
   | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
   | RCases (_,rtntypopt,tml,pl) ->
       RCases (dummy_loc,
@@ -69,7 +69,7 @@ let rec unloc = function
   | RRec (_,fk,idl,bl,tyl,bv) ->
       RRec (dummy_loc,fk,idl,
             Array.map (List.map 
-              (fun (na,obd,ty) -> (na,Option.map unloc obd, unloc ty)))
+              (fun (na,k,obd,ty) -> (na,k,Option.map unloc obd, unloc ty)))
               bl,
             Array.map unloc tyl,
             Array.map unloc bv)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index e29f172109..2994bc3aea 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -74,9 +74,9 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
       let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in
       subst_rawvars outerl it
   | ALambda (na,ty,c) ->
-      let e,na = name_fold_map g e na in RLambda (loc,na,f e ty,f e c)
+      let e,na = name_fold_map g e na in RLambda (loc,na,Explicit,f e ty,f e c)
   | AProd (na,ty,c) ->
-      let e,na = name_fold_map g e na in RProd (loc,na,f e ty,f e c)
+      let e,na = name_fold_map g e na in RProd (loc,na,Explicit,f e ty,f e c)
   | ALetIn (na,b,c) ->
       let e,na = name_fold_map g e na in RLetIn (loc,na,f e b,f e c)
   | ACases (rtntypopt,tml,eqnl) ->
@@ -131,9 +131,9 @@ let compare_rawconstr f t1 t2 = match t1,t2 with
   | RRef (_,r1), RRef (_,r2) -> r1 = r2
   | RVar (_,v1), RVar (_,v2) -> v1 = v2
   | RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & List.for_all2 f l1 l2
-  | RLambda (_,na1,ty1,c1), RLambda (_,na2,ty2,c2) when na1 = na2 ->
+  | RLambda (_,na1,bk1,ty1,c1), RLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 ->
       f ty1 ty2 & f c1 c2
-  | RProd (_,na1,ty1,c1), RProd (_,na2,ty2,c2) when na1 = na2 ->
+  | RProd (_,na1,bk1,ty1,c1), RProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 ->
       f ty1 ty2 & f c1 c2
   | RHole _, RHole _ -> true
   | RSort (_,s1), RSort (_,s2) -> s1 = s2
@@ -180,8 +180,8 @@ let aconstr_and_vars_of_rawconstr a =
       found := ldots_var :: !found; assert lassoc;
       AList (x,y,AApp (AVar ldots_var,[AVar x]),aux t,lassoc)
   | RApp (_,g,args) -> AApp (aux g, List.map aux args)
-  | RLambda (_,na,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
-  | RProd (_,na,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
+  | RLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
+  | RProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
   | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
   | RCases (_,rtntypopt,tml,eqnl) ->
       let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in
@@ -377,7 +377,7 @@ let abstract_return_type_context pi mklam tml rtno =
 
 let abstract_return_type_context_rawconstr =
   abstract_return_type_context (fun (_,_,_,nal) -> nal)
-    (fun na c -> RLambda(dummy_loc,na,RHole(dummy_loc,Evd.InternalHole),c))
+    (fun na c -> RLambda(dummy_loc,na,Explicit,RHole(dummy_loc,Evd.InternalHole),c))
 
 let abstract_return_type_context_aconstr =
   abstract_return_type_context pi3
@@ -440,9 +440,9 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | RApp (_,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc) 
       when List.length l1 = List.length l2 ->
       match_alist alp metas sigma (f1::l1) (f2::l2) x iter termin lassoc
-  | RLambda (_,na1,t1,b1), ALambda (na2,t2,b2) ->
+  | RLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) ->
      match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
-  | RProd (_,na1,t1,b1), AProd (na2,t2,b2) ->
+  | RProd (_,na1,_,t1,b1), AProd (na2,t2,b2) ->
      match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
   | RLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) ->
      match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
@@ -530,7 +530,9 @@ let match_aconstr c (metas_scl,pat) =
 
 type notation = string
 
-type explicitation = ExplByPos of int | ExplByName of identifier
+type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
+
+type binder_kind = Default of binding_kind | TypeClass of binding_kind
 
 type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
 
@@ -550,8 +552,8 @@ type constr_expr =
   | CFix of loc * identifier located * fixpoint_expr list
   | CCoFix of loc * identifier located * cofixpoint_expr list
   | CArrow of loc * constr_expr * constr_expr
-  | CProdN of loc * (name located list * constr_expr) list * constr_expr
-  | CLambdaN of loc * (name located list * constr_expr) list * constr_expr
+  | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
+  | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
   | CLetIn of loc * name located * constr_expr * constr_expr
   | CAppExpl of loc * (proj_flag * reference) * constr_expr list
   | CApp of loc * (proj_flag * constr_expr) * 
@@ -579,7 +581,11 @@ and fixpoint_expr =
 
 and local_binder =
   | LocalRawDef of name located * constr_expr
-  | LocalRawAssum of name located list * constr_expr
+  | LocalRawAssum of name located list * binder_kind * constr_expr
+      
+and typeclass_constraint = name located * binding_kind * constr_expr
+
+and typeclass_context = typeclass_constraint list
 
 and cofixpoint_expr =
     identifier * local_binder list * constr_expr * constr_expr
@@ -592,21 +598,23 @@ and recursion_order_expr =
 (***********************)
 (* For binders parsing *)
 
+let default_binder_kind = Default Explicit
+
 let rec local_binders_length = function
   | [] -> 0
   | LocalRawDef _::bl -> 1 + local_binders_length bl
-  | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl
+  | LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
 
 let rec local_assums_length = function
   | [] -> 0
   | LocalRawDef _::bl -> local_binders_length bl
-  | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl
+  | LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
 
 let names_of_local_assums bl =
-  List.flatten (List.map (function LocalRawAssum(l,_)->l|_->[]) bl)
+  List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl)
 
 let names_of_local_binders bl =
-  List.flatten (List.map (function LocalRawAssum(l,_)->l|LocalRawDef(l,_)->[l]) bl)
+  List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl)
 
 (**********************************************************************)
 (* Functions on constr_expr *)
@@ -684,7 +692,7 @@ let ids_of_pattern_list =
     Idset.empty
 
 let rec fold_constr_expr_binders g f n acc b = function
-  | (nal,t)::l ->
+  | (nal,bk,t)::l ->
       let nal = snd (List.split nal) in
       let n' = List.fold_right (name_fold g) nal n in
       f n (fold_constr_expr_binders g f n' acc b l) t
@@ -692,7 +700,7 @@ let rec fold_constr_expr_binders g f n acc b = function
       f n acc b
 
 let rec fold_local_binders g f n acc b = function
-  | LocalRawAssum (nal,t)::l ->
+  | LocalRawAssum (nal,bk,t)::l ->
       let nal = snd (List.split nal) in
       let n' = List.fold_right (name_fold g) nal n in
       f n (fold_local_binders g f n' acc b l) t
@@ -706,7 +714,7 @@ let fold_constr_expr_with_binders g f n acc = function
   | CAppExpl (loc,(_,_),l) -> List.fold_left (f n) acc l
   | CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
   | CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l
-  | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],a]
+  | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],default_binder_kind,a]
   | CCast (loc,a,CastConv(_,b)) -> f n (f n acc a) b
   | CCast (loc,a,CastCoerce) -> f n acc a
   | CNotation (_,_,l) -> List.fold_left (f n) acc l
@@ -746,40 +754,40 @@ let mkIdentC id  = CRef (Ident (dummy_loc, id))
 let mkRefC r     = CRef r
 let mkAppC (f,l) = CApp (dummy_loc, (None,f), List.map (fun x -> (x,None)) l)
 let mkCastC (a,k)  = CCast (dummy_loc,a,k)
-let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b)
+let mkLambdaC (idl,bk,a,b) = CLambdaN (dummy_loc,[idl,bk,a],b)
 let mkLetInC (id,a,b)   = CLetIn (dummy_loc,id,a,b)
-let mkProdC (idl,a,b)   = CProdN (dummy_loc,[idl,a],b)
+let mkProdC (idl,bk,a,b)   = CProdN (dummy_loc,[idl,bk,a],b)
 
 let rec mkCProdN loc bll c =
   match bll with
-  | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> 
-      CProdN (loc,[idl,t],mkCProdN (join_loc loc1 loc) bll c)
+  | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> 
+      CProdN (loc,[idl,bk,t],mkCProdN (join_loc loc1 loc) bll c)
   | LocalRawDef ((loc1,_) as id,b) :: bll -> 
       CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c)
   | [] -> c
-  | LocalRawAssum ([],_) :: bll -> mkCProdN loc bll c
+  | LocalRawAssum ([],_,_) :: bll -> mkCProdN loc bll c
 
 let rec mkCLambdaN loc bll c =
   match bll with
-  | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> 
-      CLambdaN (loc,[idl,t],mkCLambdaN (join_loc loc1 loc) bll c)
+  | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> 
+      CLambdaN (loc,[idl,bk,t],mkCLambdaN (join_loc loc1 loc) bll c)
   | LocalRawDef ((loc1,_) as id,b) :: bll -> 
       CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c)
   | [] -> c
-  | LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c
+  | LocalRawAssum ([],_,_) :: bll -> mkCLambdaN loc bll c
 
 let rec abstract_constr_expr c = function
   | [] -> c
   | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
-  | LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
+  | LocalRawAssum (idl,bk,t)::bl ->
+      List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
       (abstract_constr_expr c bl)
       
 let rec prod_constr_expr c = function
   | [] -> c
   | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
-  | LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> mkProdC([x],t,b)) idl
+  | LocalRawAssum (idl,bk,t)::bl ->
+      List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
       (prod_constr_expr c bl)
 
 let coerce_to_id = function
@@ -794,15 +802,15 @@ let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
 
 let map_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
-  let h (e,bl) (nal,t) = (map_binder g e nal,(nal,f e t)::bl) in
+  let h (e,bl) (nal,bk,t) = (map_binder g e nal,(nal,bk,f e t)::bl) in
   let (e,rbl) = List.fold_left h (e,[]) bl in
   (e, List.rev rbl)
 
 let map_local_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
   let h (e,bl) = function
-      LocalRawAssum(nal,ty) ->
-        (map_binder g e nal, LocalRawAssum(nal,f e ty)::bl)
+      LocalRawAssum(nal,k,ty) ->
+        (map_binder g e nal, LocalRawAssum(nal,k,f e ty)::bl)
     | LocalRawDef((loc,na),ty) ->
         (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) in
   let (e,rbl) = List.fold_left h (e,[]) bl in
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 3d928bbb4a..608cedb3c1 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -90,7 +90,9 @@ val match_aconstr : rawconstr -> interpretation ->
 
 type notation = string
 
-type explicitation = ExplByPos of int | ExplByName of identifier
+type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
+  
+type binder_kind = Default of binding_kind | TypeClass of binding_kind
 
 type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
 
@@ -110,8 +112,8 @@ type constr_expr =
   | CFix of loc * identifier located * fixpoint_expr list
   | CCoFix of loc * identifier located * cofixpoint_expr list
   | CArrow of loc * constr_expr * constr_expr
-  | CProdN of loc * (name located list * constr_expr) list * constr_expr
-  | CLambdaN of loc * (name located list * constr_expr) list * constr_expr
+  | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
+  | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
   | CLetIn of loc * name located * constr_expr * constr_expr
   | CAppExpl of loc * (proj_flag * reference) * constr_expr list
   | CApp of loc * (proj_flag * constr_expr) * 
@@ -146,7 +148,11 @@ and recursion_order_expr =
 
 and local_binder =
   | LocalRawDef of name located * constr_expr
-  | LocalRawAssum of name located list * constr_expr
+  | LocalRawAssum of name located list * binder_kind * constr_expr
+      
+type typeclass_constraint = name located * binding_kind * constr_expr
+
+and typeclass_context = typeclass_constraint list
 
 (**********************************************************************)
 (* Utilities on constr_expr                                           *)
@@ -161,6 +167,8 @@ val replace_vars_constr_expr :
 val free_vars_of_constr_expr : constr_expr -> Idset.t
 val occur_var_constr_expr : identifier -> constr_expr -> bool
 
+val default_binder_kind : binder_kind
+
 (* Specific function for interning "in indtype" syntax of "match" *)
 val ids_of_cases_indtype : constr_expr -> identifier list
 
@@ -168,9 +176,9 @@ val mkIdentC : identifier -> constr_expr
 val mkRefC : reference -> constr_expr
 val mkAppC : constr_expr * constr_expr list -> constr_expr
 val mkCastC : constr_expr * constr_expr cast_type -> constr_expr
-val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr
+val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
 val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
-val mkProdC : name located list * constr_expr * constr_expr -> constr_expr
+val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
 
 val coerce_to_id : constr_expr -> identifier located
 
@@ -195,6 +203,11 @@ val names_of_local_assums : local_binder list -> name located list
 (* With let binders *)
 val names_of_local_binders : local_binder list -> name located list
 
+(* Used in typeclasses *)
+
+val fold_constr_expr_with_binders : (identifier -> 'a -> 'a) ->
+   ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b
+
 (* Used in correctness and interface; absence of var capture not guaranteed *)
 (* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)