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

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

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


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

14 files changed, 298 insertions, 99 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 4627d2305..c649b5846 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -37,7 +37,7 @@ let mk_lam = function
   | (bl,c) -> CLambdaN(constr_loc c, bl,c)
 
 let loc_of_binder_let = function
-  | LocalRawAssum ((loc,_)::_,_)::_ -> loc
+  | LocalRawAssum ((loc,_)::_,_,_)::_ -> loc
   | LocalRawDef ((loc,_),_)::_ -> loc
   | _ -> dummy_loc
 
@@ -99,10 +99,10 @@ let lpar_id_coloneq =
               | _ -> raise Stream.Failure)
         | _ -> raise Stream.Failure)
 
-
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
-  constr_pattern lconstr_pattern Constr.ident binder binder_let pattern;
+  constr_pattern lconstr_pattern Constr.ident
+  binder binder_let binders_let typeclass_constraint typeclass_param pattern;
   Constr.ident:
     [ [ id = Prim.ident -> id
 
@@ -307,28 +307,70 @@ GEXTEND Gram
   ;
   binder_list:
     [ [ idl=LIST1 name; bl=LIST0 binder_let -> 
-          LocalRawAssum (idl,CHole loc)::bl
+          LocalRawAssum (idl,Default Explicit,CHole loc)::bl
       | idl=LIST1 name; ":"; c=lconstr -> 
-          [LocalRawAssum (idl,c)]
-      | "("; idl=LIST1 name; ":"; c=lconstr; ")"; bl=LIST0 binder_let ->
-          LocalRawAssum (idl,c)::bl ] ]
+          [LocalRawAssum (idl,Default Explicit,c)]
+      | cl = binders_let -> cl
+    ] ]
+  ;
+  binders_let: 
+    [ [ "["; ctx = LIST1 typeclass_constraint_binder SEP ","; "]"; bl=binders_let -> 
+	  ctx @ bl
+    | cl = LIST0 binder_let -> cl
+    ] ]
   ;
   binder_let:
     [ [ id=name ->
-          LocalRawAssum ([id],CHole loc)
+          LocalRawAssum ([id],Default Explicit,CHole loc)
       | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> 
-          LocalRawAssum (id::idl,c)
+          LocalRawAssum (id::idl,Default Explicit,c)
       | "("; id=name; ":"; c=lconstr; ")" -> 
-          LocalRawAssum ([id],c)
+          LocalRawAssum ([id],Default Explicit,c)
+      | "`"; id=name; "`" ->
+          LocalRawAssum ([id],Default Implicit,CHole loc)
+      | "`"; id=name; idl=LIST1 name; ":"; c=lconstr; "`" -> 
+          LocalRawAssum (id::idl,Default Implicit,c)
+      | "`"; id=name; ":"; c=lconstr; "`" -> 
+          LocalRawAssum ([id],Default Implicit,c)
+      | "`"; id=name; idl=LIST1 name; "`" -> 
+          LocalRawAssum (id::idl,Default Implicit,CHole loc)
       | "("; id=name; ":="; c=lconstr; ")" ->
           LocalRawDef (id,c)
       | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> 
           LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))
+      | "["; tc = typeclass_constraint_binder; "]" -> tc
     ] ]
   ;
   binder:
-    [ [ id=name -> ([id],CHole loc)
-      | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,c) ] ]
+    [ [ id=name -> ([id],Default Explicit,CHole loc)
+      | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c) 
+      | "`"; idl=LIST1 name; ":"; c=lconstr; "`" -> (idl,Default Implicit,c) 
+    ] ]
+  ;
+  typeclass_constraint_binder:
+    [ [ tc = typeclass_constraint ->
+      let (n,bk,t) = tc in
+	LocalRawAssum ([n], TypeClass bk, t)
+    ] ]
+  ;
+  typeclass_constraint:
+    [ [ id=identref ; cl = LIST1 typeclass_param -> 
+      (loc, Anonymous), Explicit, mkAppC (mkIdentC (snd id), cl)
+    | "?" ; id=identref ; cl = LIST1 typeclass_param -> 
+	(loc, Anonymous), Implicit, mkAppC (mkIdentC (snd id), cl)
+    | iid=identref ; ":" ; id=typeclass_name ; cl = LIST1 typeclass_param -> 
+	(fst iid, Name (snd iid)), (fst id), mkAppC (mkIdentC (snd (snd id)), cl)
+    ] ]
+  ;
+  typeclass_name:
+    [ [ id=identref -> (Explicit, id)
+    | "?"; id = identref -> (Implicit, id)
+    ] ]
+  ;
+  typeclass_param: 
+    [ [ id = identref -> CRef (Libnames.Ident id)
+    | c = sort -> CSort (loc, c)
+    | "("; c = lconstr; ")" -> c ] ]
   ;
   type_cstr:
     [ [ c=OPT [":"; c=lconstr -> c] -> (loc,c) ] ]
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 3c5c88e89..79e88f8cd 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -215,12 +215,17 @@ GEXTEND Gram
       | n = integer -> MsgInt n ] ]
   ;
 
+  ltac_def_kind:
+    [ [ ":=" -> false
+      | "::=" -> true ] ]
+  ;
+	
   (* Definitions for tactics *)
   tacdef_body:
-    [ [ name = identref; it=LIST1 input_fun; ":="; body = tactic_expr ->
-	  (name, TacFun (it, body))
-      | name = identref; ":="; body = tactic_expr ->
-	  (name, body) ] ]
+    [ [ name = identref; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr ->
+	  (name, redef, TacFun (it, body))
+      | name = identref; redef = ltac_def_kind; body = tactic_expr ->
+	  (name, redef, body) ] ]
   ;
   tactic:
     [ [ tac = tactic_expr -> tac ] ]
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 23e4ba621..f305ebd69 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -95,9 +95,9 @@ open Tactic
 let mk_fix_tac (loc,id,bl,ann,ty) =
   let n =
     match bl,ann with
-        [([_],_)], None -> 1
+        [([_],_,_)], None -> 1
       | _, Some x ->
-          let ids = List.map snd (List.flatten (List.map fst bl)) in
+          let ids = List.map snd (List.flatten (List.map pi1 bl)) in
           (try list_index (snd x) ids
           with Not_found -> error "no such fix variable")
       | _ -> error "cannot guess decreasing argument of fix" in
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 729693aa7..ee2036167 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -46,6 +46,7 @@ let noedit_mode = Gram.Entry.create "vernac:noedit_command"
 let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
 let thm_token = Gram.Entry.create "vernac:thm_token"
 let def_body = Gram.Entry.create "vernac:def_body"
+let typeclass_context = Gram.Entry.create "vernac:typeclass_context"
 
 let get_command_entry () =
   match Decl_mode.get_current_mode () with
@@ -116,11 +117,11 @@ let no_coercion loc (c,x) =
 
 (* Gallina declarations *)
 GEXTEND Gram
-  GLOBAL: gallina gallina_ext thm_token def_body;
+  GLOBAL: gallina gallina_ext thm_token def_body typeclass_context typeclass_constraint;
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = identref; bl = LIST0 binder_let; ":";
+    [ [ thm = thm_token; id = identref; bl = binders_let; ":";
         c = lconstr ->
           VernacStartTheoremProof (thm, id, (bl, c), false, no_hook)
       | stre = assumption_token; nl = inline; bl = assum_list -> 
@@ -164,6 +165,10 @@ GEXTEND Gram
 *)
     ] ]
   ;
+  typeclass_context:
+    [ [ "["; l=LIST1 typeclass_constraint SEP ","; "]" -> l 
+    | -> [] ] ]
+  ;
   thm_token:
     [ [ "Theorem" -> Theorem
       | IDENT "Lemma" -> Lemma
@@ -209,14 +214,14 @@ GEXTEND Gram
   ;
   (* Simple definitions *)
   def_body:
-    [ [ bl = LIST0 binder_let; ":="; red = reduce; c = lconstr ->
+    [ [ bl = binders_let; ":="; red = reduce; c = lconstr ->
       (match c with
           CCast(_,c, Rawterm.CastConv (k,t)) -> DefineBody (bl, red, c, Some t)
         | _ -> DefineBody (bl, red, c, None))
-      | bl = LIST0 binder_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
-          DefineBody (bl, red, c, Some t)
-      | bl = LIST0 binder_let; ":"; t = lconstr ->
-          ProveBody (bl, t) ] ]
+    | bl = binders_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
+	DefineBody (bl, red, c, Some t)
+    | bl = binders_let; ":"; t = lconstr ->
+        ProveBody (bl, t) ] ]
   ;
   reduce:
     [ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r
@@ -431,7 +436,7 @@ END
 
 (* Extensions: implicits, coercions, etc. *)   
 GEXTEND Gram
-  GLOBAL: gallina_ext;
+  GLOBAL: gallina_ext typeclass_param;
 
   gallina_ext:
     [ [ (* Transparent and Opaque *)
@@ -467,22 +472,68 @@ GEXTEND Gram
          t = class_rawexpr ->
 	  VernacCoercion (Global, qid, s, t)
 
+      (* Type classes *)
+      | IDENT "Class"; sup = OPT [ l = typeclass_context; "=>" -> l ];
+	 qid = identref; pars = LIST0 typeclass_param_type;
+	 s = [ ":"; c = sort -> loc, c | -> (loc,Rawterm.RType None) ];
+	 props = typeclass_field_types ->
+	   VernacClass (qid, pars, s, (match sup with None -> [] | Some l -> l), props)
+	     
+      | IDENT "Context"; c = typeclass_context -> 
+	  VernacContext c
+
+      | IDENT "Instance"; sup = OPT [ l = typeclass_context ; "=>" -> l ];
+	 is = typeclass_constraint ; props = typeclass_field_defs ->
+	   let sup = match sup with None -> [] | Some l -> l in
+	     VernacInstance (sup, is, props)
+
+      | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is
+
+      | IDENT "Instantiation"; IDENT "Tactic"; ":="; tac = Tactic.tactic -> 
+	  VernacSetInstantiationTactic tac
+
       (* Implicit *)
-      | IDENT "Implicit"; IDENT "Arguments"; 
+      | IDENT "Implicit"; IDENT "Arguments"; enrich = [ IDENT "Enriching" -> true | -> false ];
 	 (local,qid,pos) = 
 	     [ local = [ IDENT "Global" -> false | IDENT "Local" -> true ];
 	       qid = global -> (local,qid,None) 
 	     | qid = global;
 	       l = OPT [ "["; l = LIST0 implicit_name; "]" -> 
-		   List.map (fun (id,b) -> (ExplByName id,b)) l ] ->
+		   List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
 		 (true,qid,l) ] ->
-	   VernacDeclareImplicits (local,qid,pos)
+	   VernacDeclareImplicits (local,qid,enrich,pos)
 
       | IDENT "Implicit"; ["Type" | IDENT "Types"];
 	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ]
   ;
+
+(*   typeclass_ctx:  *)
+(*     [ [ sup = LIST1 operconstr SEP "->"; "=>" -> sup *)
+(*     ] ] *)
+(*   ; *)
   implicit_name:
-    [ [ id = ident -> (id,false) | "["; id = ident; "]" -> (id,true) ] ]
+    [ [ "!"; id = ident -> (id, false, true)
+    | id = ident -> (id,false,false)
+    | "["; "!"; id = ident; "]" -> (id,true,true) 
+    | "["; id = ident; "]" -> (id,true, false) ] ]
+  ;
+  typeclass_param_type:
+    [ [ "(" ; id = identref; ":"; t = lconstr ; ")" -> id, t 
+    | id = identref -> id, CHole loc ] ]
+  ;
+  typeclass_field_type:
+    [ [ id = identref; ":"; t = lconstr -> id, t ] ]
+  ;
+  typeclass_field_def:
+    [ [ id = identref; params = LIST0 identref; ":="; t = lconstr -> id, params, t ] ]
+  ;
+  typeclass_field_types:
+    [ [ ":="; l = LIST1 typeclass_field_type SEP ";" -> l
+    | -> [] ] ]
+  ;
+  typeclass_field_defs:
+    [ [ ":="; l = LIST1 typeclass_field_def SEP ";" -> l
+    | -> [] ] ]
   ;
 END
 
@@ -614,6 +665,8 @@ GEXTEND Gram
       | IDENT "ML"; IDENT "Modules" -> PrintMLModules
       | IDENT "Graph" -> PrintGraph
       | IDENT "Classes" ->  PrintClasses
+      | IDENT "TypeClasses" -> PrintTypeClasses
+      | IDENT "Instances"; qid = global -> PrintInstances qid
       | IDENT "Ltac"; qid = global -> PrintLtac qid
       | IDENT "Coercions" -> PrintCoercions
       | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index cd929e5af..47725cbd6 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -141,12 +141,12 @@ let rec interp_xml_constr = function
   | XmlTag (loc,"LAMBDA",al,(_::_ as xl)) ->
       let body,decls = list_sep_last xl in
       let ctx = List.map interp_xml_decl decls in
-      List.fold_right (fun (na,t) b -> RLambda (loc, na, t, b))
+      List.fold_right (fun (na,t) b -> RLambda (loc, na, Explicit, t, b))
 	ctx (interp_xml_target body)
   | XmlTag (loc,"PROD",al,(_::_ as xl)) ->
       let body,decls = list_sep_last xl in
       let ctx = List.map interp_xml_decl decls in
-      List.fold_right (fun (na,t) b -> RProd (loc, na, t, b))
+      List.fold_right (fun (na,t) b -> RProd (loc, na, Explicit, t, b))
 	ctx (interp_xml_target body)
   | XmlTag (loc,"LETIN",al,(_::_ as xl)) ->
       let body,defs = list_sep_last xl in
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index d2380dad6..56d547cb5 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -434,6 +434,9 @@ module Constr =
     let lconstr_pattern = gec_constr "lconstr_pattern"
     let binder = Gram.Entry.create "constr:binder"
     let binder_let = Gram.Entry.create "constr:binder_let"
+    let binders_let = Gram.Entry.create "constr:binders_let"
+    let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint"
+    let typeclass_param = Gram.Entry.create "constr:typeclass_param"
   end
 
 module Module =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 651554486..eaf298e06 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -161,8 +161,11 @@ module Constr :
     val annot : constr_expr Gram.Entry.e
     val constr_pattern : constr_expr Gram.Entry.e
     val lconstr_pattern : constr_expr Gram.Entry.e
-    val binder : (name located list * constr_expr) Gram.Entry.e
+    val binder : (name located list * binder_kind * constr_expr) Gram.Entry.e
     val binder_let : local_binder Gram.Entry.e
+    val binders_let : local_binder list Gram.Entry.e
+    val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
+    val typeclass_param : constr_expr Gram.Entry.e
   end
 
 module Module : 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 858c6685f..85bf11806 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -129,7 +129,7 @@ let pr_qualid = pr_qualid
 let pr_expl_args pr (a,expl) =
   match expl with
   | None -> pr (lapp,L) a
-  | Some (_,ExplByPos n) ->
+  | Some (_,ExplByPos (n,_id)) ->
       anomaly("Explicitation by position not implemented")
   | Some (_,ExplByName id) -> 
       str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
@@ -206,30 +206,41 @@ let pr_eqn pr (loc,pl,rhs) =
 
 let begin_of_binder = function
     LocalRawDef((loc,_),_) -> fst (unloc loc)
-  | LocalRawAssum((loc,_)::_,_) -> fst (unloc loc)
+  | LocalRawAssum((loc,_)::_,_,_) -> fst (unloc loc)
   | _ -> assert false
 
 let begin_of_binders = function
   | b::_ -> begin_of_binder b
   | _ -> 0
 
-let pr_binder many pr (nal,t) =
+let surround_binder k p = 
+  match k with
+      Default Explicit -> hov 1 (str"(" ++ p ++ str")")
+    | Default Implicit -> hov 1 (str"`" ++ p ++ str"`")
+    | TypeClass b -> hov 1 (str"[" ++ p ++ str"]")
+
+let surround_implicit k p =
+  match k with
+      Default Explicit -> p
+    | Default Implicit -> (str"`" ++ p ++ str"`")
+    | TypeClass b -> (str"[" ++ p ++ str"]")
+
+let pr_binder many pr (nal,k,t) =
   match t with
   | CHole _ -> prlist_with_sep spc pr_lname nal
   | _ ->
     let s = prlist_with_sep spc pr_lname nal ++ str" : " ++ pr t in
-    hov 1 (if many then surround s else s)
+      hov 1 (if many then surround_binder k s else surround_implicit k s)
 
 let pr_binder_among_many pr_c = function
-  | LocalRawAssum (nal,t) ->
-      pr_binder true pr_c (nal,t)
+  | LocalRawAssum (nal,k,t) ->
+      pr_binder true pr_c (nal,k,t)
   | LocalRawDef (na,c) ->
       let c,topt = match c with
         | CCast(_,c, CastConv (_,t)) -> c, t
         | _ -> c, CHole dummy_loc in
-      hov 1 (surround
-        (pr_lname na ++ pr_opt_type pr_c topt ++
-         str":=" ++ cut() ++ pr_c c))
+      hov 1 (pr_lname na ++ pr_opt_type pr_c topt ++
+         str":=" ++ cut() ++ pr_c c)
 
 let pr_undelimited_binders pr_c =
   prlist_with_sep spc (pr_binder_among_many pr_c)
@@ -237,8 +248,8 @@ let pr_undelimited_binders pr_c =
 let pr_delimited_binders kw pr_c bl =
   let n = begin_of_binders bl in
   match bl with
-  | [LocalRawAssum (nal,t)] ->
-      pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,t)
+  | [LocalRawAssum (nal,k,t)] ->
+      pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t)
   | LocalRawAssum _ :: _ as bdl ->
       pr_com_at n ++ kw() ++ pr_undelimited_binders pr_c bdl
   | _ -> assert false
@@ -249,9 +260,9 @@ let rec extract_prod_binders = function
       if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
   | CProdN (loc,[],c) ->
       extract_prod_binders c
-  | CProdN (loc,(nal,t)::bl,c) ->
+  | CProdN (loc,(nal,bk,t)::bl,c) ->
       let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in
-      LocalRawAssum (nal,t) :: bl, c
+      LocalRawAssum (nal,bk,t) :: bl, c
   | c -> [], c
 
 let rec extract_lam_binders = function
@@ -260,15 +271,15 @@ let rec extract_lam_binders = function
       if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
   | CLambdaN (loc,[],c) ->
       extract_lam_binders c
-  | CLambdaN (loc,(nal,t)::bl,c) ->
+  | CLambdaN (loc,(nal,bk,t)::bl,c) ->
       let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in
-      LocalRawAssum (nal,t) :: bl, c
+      LocalRawAssum (nal,bk,t) :: bl, c
   | c -> [], c
     
 let split_lambda = function
-  | CLambdaN (loc,[[na],t],c) -> (na,t,c)
-  | CLambdaN (loc,([na],t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
-  | CLambdaN (loc,(na::nal,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,t)::bl,c))
+  | CLambdaN (loc,[[na],bk,t],c) -> (na,t,c)
+  | CLambdaN (loc,([na],bk,t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
+  | CLambdaN (loc,(na::nal,bk,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,bk,t)::bl,c))
   | _ -> anomaly "ill-formed fixpoint body"
 
 let rename na na' t c =
@@ -279,13 +290,13 @@ let rename na na' t c =
   
 let split_product na' = function
   | CArrow (loc,t,c) -> (na',t,c)
-  | CProdN (loc,[[na],t],c) -> rename na na' t c
-  | CProdN (loc,([na],t)::bl,c) -> rename na na' t (CProdN(loc,bl,c))
-  | CProdN (loc,(na::nal,t)::bl,c) ->
-      rename na na' t (CProdN(loc,(nal,t)::bl,c))
+  | CProdN (loc,[[na],bk,t],c) -> rename na na' t c
+  | CProdN (loc,([na],bk,t)::bl,c) -> rename na na' t (CProdN(loc,bl,c))
+  | CProdN (loc,(na::nal,bk,t)::bl,c) ->
+      rename na na' t (CProdN(loc,(nal,bk,t)::bl,c))
   | _ -> anomaly "ill-formed fixpoint body"
 
-let merge_binders (na1,ty1) cofun (na2,ty2) codom =
+let merge_binders (na1,bk1,ty1) cofun (na2,bk2,ty2) codom =
   let na =
     match snd na1, snd na2 with
         Anonymous, Name id ->
@@ -306,42 +317,42 @@ let merge_binders (na1,ty1) cofun (na2,ty2) codom =
       | _ ->
           Constrextern.check_same_type ty1 ty2;
           ty2 in
-  (LocalRawAssum ([na],ty), codom)
+  (LocalRawAssum ([na],bk1,ty), codom)
             
 let rec strip_domain bvar cofun c =
   match c with
     | CArrow(loc,a,b) ->
-        merge_binders bvar cofun ((dummy_loc,Anonymous),a) b
-    | CProdN(loc,[([na],ty)],c') ->
-        merge_binders bvar cofun (na,ty) c'
-    | CProdN(loc,([na],ty)::bl,c') ->
-        merge_binders bvar cofun (na,ty) (CProdN(loc,bl,c'))
-    | CProdN(loc,(na::nal,ty)::bl,c') ->
-        merge_binders bvar cofun (na,ty) (CProdN(loc,(nal,ty)::bl,c'))
+        merge_binders bvar cofun ((dummy_loc,Anonymous),default_binder_kind,a) b
+    | CProdN(loc,[([na],bk,ty)],c') ->
+        merge_binders bvar cofun (na,bk,ty) c'
+    | CProdN(loc,([na],bk,ty)::bl,c') ->
+        merge_binders bvar cofun (na,bk,ty) (CProdN(loc,bl,c'))
+    | CProdN(loc,(na::nal,bk,ty)::bl,c') ->
+        merge_binders bvar cofun (na,bk,ty) (CProdN(loc,(nal,bk,ty)::bl,c'))
     | _ -> failwith "not a product"
 
 (* Note: binder sharing is lost *)
-let rec strip_domains (nal,ty) cofun c =
+let rec strip_domains (nal,bk,ty) cofun c =
   match nal with
       [] -> assert false
     | [na] ->
-        let bnd, c' = strip_domain (na,ty) cofun c in
+        let bnd, c' = strip_domain (na,bk,ty) cofun c in
         ([bnd],None,c')
     | na::nal ->
-        let f = CLambdaN(dummy_loc,[(nal,ty)],cofun) in
-        let bnd, c1 = strip_domain (na,ty) f c in
+        let f = CLambdaN(dummy_loc,[(nal,bk,ty)],cofun) in
+        let bnd, c1 = strip_domain (na,bk,ty) f c in
         (try
-          let bl, rest, c2 = strip_domains (nal,ty) cofun c1 in
+          let bl, rest, c2 = strip_domains (nal,bk,ty) cofun c1 in
           (bnd::bl, rest, c2)
-        with Failure _ -> ([bnd],Some (nal,ty), c1))
+        with Failure _ -> ([bnd],Some (nal,bk,ty), c1))
 
 (* Re-share binders *)
 let rec factorize_binders = function
   | ([] | [_] as l) -> l
-  | LocalRawAssum (nal,ty) as d :: (LocalRawAssum (nal',ty')::l as l') ->
+  | LocalRawAssum (nal,k,ty) as d :: (LocalRawAssum (nal',k',ty')::l as l') ->
       (try
 	let _ = Constrextern.check_same_type ty ty' in
-	factorize_binders (LocalRawAssum (nal@nal',ty)::l)
+	factorize_binders (LocalRawAssum (nal@nal',k,ty)::l)
       with _ ->
 	d :: factorize_binders l')
   | d :: l -> d :: factorize_binders l
@@ -370,7 +381,7 @@ let rec split_fix n typ def =
     let (na,_,def) = split_lambda def in
     let (na,t,typ) = split_product na typ in
     let (bl,typ,def) = split_fix (n-1) typ def in
-    (LocalRawAssum ([na],t)::bl,typ,def)
+    (LocalRawAssum ([na],default_binder_kind,t)::bl,typ,def)
 
 let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
   let pr_body =
@@ -601,27 +612,27 @@ let rec strip_context n iscast t =
   if n = 0 then
     [], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t
   else match t with
-    | CLambdaN (loc,(nal,t)::bll,c) ->
+    | CLambdaN (loc,(nal,bk,t)::bll,c) ->
 	let n' = List.length nal in
 	if n' > n then
 	  let nal1,nal2 = list_chop n nal in
-	  [LocalRawAssum (nal1,t)], CLambdaN (loc,(nal2,t)::bll,c)
+	  [LocalRawAssum (nal1,bk,t)], CLambdaN (loc,(nal2,bk,t)::bll,c)
 	else
 	let bl', c = strip_context (n-n') iscast
 	  (if bll=[] then c else CLambdaN (loc,bll,c)) in
-	LocalRawAssum (nal,t) :: bl', c 
-    | CProdN (loc,(nal,t)::bll,c) ->
+	LocalRawAssum (nal,bk,t) :: bl', c 
+    | CProdN (loc,(nal,bk,t)::bll,c) ->
 	let n' = List.length nal in
 	if n' > n then
 	  let nal1,nal2 = list_chop n nal in
-	  [LocalRawAssum (nal1,t)], CProdN (loc,(nal2,t)::bll,c)
+	  [LocalRawAssum (nal1,bk,t)], CProdN (loc,(nal2,bk,t)::bll,c)
 	else
 	let bl', c = strip_context (n-n') iscast
 	  (if bll=[] then c else CProdN (loc,bll,c)) in
-	LocalRawAssum (nal,t) :: bl', c 
+	LocalRawAssum (nal,bk,t) :: bl', c 
     | CArrow (loc,t,c) ->
 	let bl', c = strip_context (n-1) iscast c in
-	LocalRawAssum ([loc,Anonymous],t) :: bl', c 
+	LocalRawAssum ([loc,Anonymous],default_binder_kind,t) :: bl', c
     | CCast (_,c,_) -> strip_context n false c
     | CLetIn (_,na,b,c) -> 
 	let bl', c = strip_context (n-1) iscast c in
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 019063527..7d83cffb6 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -302,9 +302,10 @@ let strip_prod_binders_expr n ty =
     match ty with
         Topconstr.CProdN(_,bll,a) ->
           let nb =
-            List.fold_left (fun i (nal,_) -> i + List.length nal) 0 bll in
-          if nb >= n then (List.rev (bll@acc), a)
-          else strip_ty (bll@acc) (n-nb) a
+            List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in
+	  let bll = List.map (fun (x, _, y) -> x, y) bll in
+            if nb >= n then (List.rev (bll@acc)), a
+            else strip_ty (bll@acc) (n-nb) a
       | Topconstr.CArrow(_,a,b) ->
           if n=1 then
             (List.rev (([(dummy_loc,Anonymous)],a)::acc), b)
@@ -978,7 +979,7 @@ let strip_prod_binders_rawterm n (ty,_) =
   let rec strip_ty acc n ty =
     if n=0 then (List.rev acc, (ty,None)) else
       match ty with
-          Rawterm.RProd(loc,na,a,b) ->
+          Rawterm.RProd(loc,na,Explicit,a,b) ->
             strip_ty (([dummy_loc,na],(a,None))::acc) (n-1) b
         | _ -> error "Cannot translate fix tactic: not enough products" in
   strip_ty [] n ty
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 1161c3b61..1470f6902 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -146,11 +146,12 @@ let pr_search a b pr_p = match a with
 let pr_locality local = if local then str "Local " else str ""
 let pr_non_globality local = if local then str "" else str "Global "
 
-let pr_explanation (e,b) =
+let pr_explanation (e,b,f) =
   let a = match e with
-  | ExplByPos n -> anomaly "No more supported"
+  | ExplByPos (n,_) -> anomaly "No more supported"
   | ExplByName id -> pr_id id in
-  if b then str "[" ++ a ++ str "]" else a
+  let a = if f then str"!" ++ a else a in
+    if b then str "[" ++ a ++ str "]" else a
 
 let pr_class_rawexpr = function
   | FunClass -> str"Funclass"
@@ -394,6 +395,18 @@ let make_pr_vernac pr_constr pr_lconstr =
 let pr_constrarg c = spc () ++ pr_constr c in
 let pr_lconstrarg c = spc () ++ pr_lconstr c in
 let pr_intarg n = spc () ++ int n in
+let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in
+let pr_lname_lident_constr (oi,bk,a) = 
+  (match snd oi with Anonymous -> mt () | Name id -> pr_lident (fst oi, id) ++ spc () ++ str":" ++ spc ()) 
+  ++ pr_lconstr a in
+let pr_typeclass_context l = 
+  match l with
+      [] -> mt ()
+    | _ -> str"[" ++ spc () ++ prlist_with_sep (fun () -> str"," ++ spc()) pr_lname_lident_constr l
+	++ spc () ++ str"]" ++ spc ()
+in
+let pr_instance_def sep (i,l,c) = pr_lident i ++ prlist_with_sep spc pr_lident l 
+  ++ sep ++ pr_constrarg c in
 
 let rec pr_vernac = function
   
@@ -565,7 +578,7 @@ let rec pr_vernac = function
 
   | VernacFixpoint (recs,b) ->
       let name_of_binder = function
-        | LocalRawAssum (nal,_) -> nal
+        | LocalRawAssum (nal,_,_) -> nal
         | LocalRawDef (_,_) -> [] in
       let pr_onerec = function
         | (id,(n,ro),bl,type_,def),ntn ->
@@ -679,6 +692,39 @@ let rec pr_vernac = function
 	spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
 	spc() ++ pr_class_rawexpr c2)
 
+
+  | VernacClass (id, par, ar, sup, props) ->
+      hov 1 (
+	str"Class" ++ spc () ++ pr_lident id ++
+	  prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++ 
+	  spc () ++ str":" ++ spc() ++ pr_rawsort (snd ar) ++
+	  spc () ++ str"where" ++ spc () ++
+	  prlist_with_sep (fun () -> str";" ++ spc()) (pr_lident_constr (spc () ++ str":" ++ spc())) props )
+	  
+	
+ | VernacInstance (sup, (instid, bk, cl), props) -> 
+     hov 1 (
+       str"Instance" ++ spc () ++ 
+	 pr_typeclass_context sup ++
+	 str"=>" ++ spc () ++ 
+	 (match snd instid with Name id -> pr_lident (fst instid, id) ++ spc () ++ str":" ++ spc () | Anonymous -> mt ()) ++
+	 pr_constr_expr cl ++ spc () ++
+	 spc () ++ str"where" ++ spc () ++
+	 prlist_with_sep (fun () -> str";" ++ spc()) (pr_instance_def (spc () ++ str":=" ++ spc())) props)
+
+ | VernacContext l ->
+     hov 1 (
+       str"Context" ++ spc () ++ str"[" ++ spc () ++
+	 prlist_with_sep (fun () -> str"," ++ spc()) pr_lname_lident_constr l ++
+	 spc () ++ str "]")
+	      
+
+ | VernacDeclareInstance id ->
+     hov 1 (str"Instance" ++ spc () ++ pr_lident id)
+       
+ | VernacSetInstantiationTactic tac ->
+     hov 1 (str"Instantiation Tactic :=" ++ spc () ++ pr_raw_tactic tac)
+
   (* Modules and Module Types *)
   | VernacDefineModule (export,m,bl,ty,bd) ->
       let b = pr_module_binders_list bl pr_lconstr in 
@@ -738,7 +784,7 @@ let rec pr_vernac = function
 
   (* Commands *)
   | VernacDeclareTacticDefinition (rc,l) ->
-      let pr_tac_body (id, body) =
+      let pr_tac_body (id, redef, body) =
         let idl, body =
           match body with
 	    | Tacexpr.TacFun (idl,b) -> idl,b
@@ -746,10 +792,10 @@ let rec pr_vernac = function
         pr_located pr_ltac_id id ++ 
 	prlist (function None -> str " _"
                        | Some id -> spc () ++ pr_id id) idl
-	++ str" :=" ++ brk(1,1) ++
+	++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
 	let idl = List.map Option.get (List.filter (fun x -> not (x=None)) idl)in
         pr_raw_tactic_env 
-	  (idl @ List.map snd (List.map fst l))
+	  (idl @ List.map snd (List.map (fun (x, _, _) -> x) l))
 	  (Global.env())
 	  body in
       hov 1
@@ -765,9 +811,9 @@ let rec pr_vernac = function
         (str"Notation " ++ pr_locality local ++ pr_id id ++ str" :=" ++
          pr_constrarg c ++
          pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
-  | VernacDeclareImplicits (local,q,None) ->
+  | VernacDeclareImplicits (local,q,e,None) ->
       hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q)
-  | VernacDeclareImplicits (local,q,Some imps) ->
+  | VernacDeclareImplicits (local,q,e,Some imps) ->
       hov 1 (str"Implicit Arguments" ++ pr_non_globality local ++
       spc() ++ pr_reference q ++ spc() ++
              str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
@@ -810,6 +856,8 @@ let rec pr_vernac = function
 	| PrintMLModules -> str"Print ML Modules"
 	| PrintGraph -> str"Print Graph"
 	| PrintClasses -> str"Print Classes"
+	| PrintTypeClasses -> str"Print TypeClasses"
+	| PrintInstances qid -> str"Print Instances" ++ spc () ++ pr_reference qid
 	| PrintLtac qid -> str"Print Ltac" ++ spc() ++ pr_reference qid
 	| PrintCoercions -> str"Print Coercions"
 	| PrintCoercionPaths (s,t) -> str"Print Coercion Paths" ++ spc() ++ pr_class_rawexpr s ++ spc() ++ pr_class_rawexpr t
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index e92db84fe..6fe4d80d4 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -746,3 +746,22 @@ let print_canonical_projections () =
 
 (*************************************************************************)
 
+(*************************************************************************)
+(* Pretty-printing functions for type classes                     *)
+
+open Typeclasses
+
+let pr_typeclass env t = 
+  gallina_print_inductive (fst t.cl_impl)
+
+let print_typeclasses () =
+  let env = Global.env () in
+    prlist_with_sep pr_spc (pr_typeclass env) (typeclasses ())
+
+let pr_instance env i = 
+  gallina_print_constant_with_infos i.is_impl
+
+let print_instances r =
+  let env = Global.env () in
+  let inst = instances r in 
+    prlist_with_sep pr_spc (pr_instance env) inst
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index df16e3526..35e23d923 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -58,6 +58,11 @@ val print_coercions : unit -> std_ppcmds
 val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds
 val print_canonical_projections : unit -> std_ppcmds
 
+(* Pretty-printing functions for type classes and instances *)
+val print_typeclasses : unit -> std_ppcmds
+val print_instances : reference -> std_ppcmds
+
+
 val inspect : int -> std_ppcmds
 
 (* Locate *)
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index d8ce0a570..497b8a3c6 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -49,9 +49,9 @@ EXTEND
   constr:
     [ "200" RIGHTA
       [ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr ->
-        <:expr< Rawterm.RProd ($dloc$,Name $id$,$c1$,$c2$) >>
+        <:expr< Rawterm.RProd ($dloc$,Name $id$,Rawterm.Explicit,$c1$,$c2$) >>
       | "fun"; id = ident; ":"; c1 = constr; "=>"; c2 = constr ->
-        <:expr< Rawterm.RLambda ($dloc$,Name $id$,$c1$,$c2$) >>
+        <:expr< Rawterm.RLambda ($dloc$,Name $id$,Rawterm.Explicit,$c1$,$c2$) >>
       | "let"; id = ident; ":="; c1 = constr; "in"; c2 = constr ->
         <:expr< Rawterm.RLetin ($dloc$,Name $id$,$c1$,$c2$) >>
       (* fix todo *)
@@ -61,7 +61,7 @@ EXTEND
         <:expr< Rawterm.RCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ]
     | "90" RIGHTA
       [ c1 = constr; "->"; c2 = SELF -> 
-        <:expr< Rawterm.RProd ($dloc$,Anonymous,$c1$,$c2$) >> ]
+        <:expr< Rawterm.RProd ($dloc$,Anonymous,Rawterm.Explicit,$c1$,$c2$) >> ]
     | "75" RIGHTA
       [ "~"; c = constr -> 
         apply_ref <:expr< coq_not_ref >> [c] ]
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index fbd2e6e07..6fdfba23d 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -129,8 +129,16 @@ let mlexpr_of_red_flags {
 
 let mlexpr_of_explicitation = function
   | Topconstr.ExplByName id -> <:expr< Topconstr.ExplByName $mlexpr_of_ident id$ >>
-  | Topconstr.ExplByPos n -> <:expr< Topconstr.ExplByPos $mlexpr_of_int n$ >>
+  | Topconstr.ExplByPos (n,_id) -> <:expr< Topconstr.ExplByPos $mlexpr_of_int n$ >>
  
+let mlexpr_of_binding_kind = function
+  | Rawterm.Implicit -> <:expr< Rawterm.Implicit >>
+  | Rawterm.Explicit -> <:expr< Rawterm.Explicit >>
+
+let mlexpr_of_binder_kind = function
+  | Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >>
+  | Topconstr.TypeClass b -> <:expr< Topconstr.TypeClass $mlexpr_of_binding_kind b$ >>
+
 let rec mlexpr_of_constr = function
   | Topconstr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) ->
       anti loc (string_of_id id)
@@ -139,8 +147,9 @@ let rec mlexpr_of_constr = function
   | Topconstr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.CArrow (loc,a,b) ->
   <:expr< Topconstr.CArrow $dloc$ $mlexpr_of_constr a$ $mlexpr_of_constr b$ >>
-  | Topconstr.CProdN (loc,l,a) -> <:expr< Topconstr.CProdN $dloc$ $mlexpr_of_list (mlexpr_of_pair (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
-  | Topconstr.CLambdaN (loc,l,a) -> <:expr< Topconstr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_pair (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
+  | Topconstr.CProdN (loc,l,a) -> <:expr< Topconstr.CProdN $dloc$ $mlexpr_of_list 
+      (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
+  | Topconstr.CLambdaN (loc,l,a) -> <:expr< Topconstr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
   | Topconstr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
   | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >>