Nouvelle syntaxe des classes

git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@1997 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

29 files changed, 2881 insertions, 1973 deletions

diff --git a/typing/btype.ml b/typing/btype.ml
index e1bd4c9f7a..67bc2520ac 100644
--- a/typing/btype.ml
+++ b/typing/btype.ml
@@ -32,6 +32,11 @@ let newmarkedgenvar () = { desc = Tvar; level = pivot_level - generic_level }
 
 (**** Representative of a type ****)
 
+let rec field_kind_repr =
+  function
+    Fvar {contents = Some kind} -> field_kind_repr kind
+  | kind                        -> kind
+
 let rec repr =
   function
     {desc = Tlink t'} ->
@@ -42,12 +47,10 @@ let rec repr =
          unification).
       *)
       repr t'
+  | {desc = Tfield (_, k, _, t')} when field_kind_repr k = Fabsent ->
+      repr t'
   | t -> t
 
-let rec field_kind_repr =
-  function
-    Fvar {contents = Some kind} -> field_kind_repr kind
-  | kind                        -> kind
 
                   (**********************************)
                   (*  Utilities for type traversal  *)
@@ -73,11 +76,19 @@ let saved_desc = ref []
 let save_desc ty desc = 
   saved_desc := (ty, desc)::!saved_desc
 
-(* Restored type descriptions *)
+(* Restored type descriptions. *)
 let cleanup_types () =
   List.iter (fun (ty, desc) -> ty.desc <- desc) !saved_desc;
   saved_desc := []
 
+(* Mark a type. *)
+let rec mark_type ty =
+  let ty = repr ty in
+  if ty.level >= lowest_level then begin
+    ty.level <- pivot_level - ty.level;
+    iter_type_expr mark_type ty
+  end
+
 (* Remove marks from a type. *)
 let rec unmark_type ty =
   let ty = repr ty in
@@ -86,6 +97,34 @@ let rec unmark_type ty =
     iter_type_expr unmark_type ty
   end
 
+let unmark_type_decl decl =
+  List.iter unmark_type decl.type_params;
+  begin match decl.type_kind with
+    Type_abstract -> ()
+  | Type_variant cstrs ->
+      List.iter (fun (c, tl) -> List.iter unmark_type tl) cstrs
+  | Type_record lbls ->
+      List.iter (fun (c, mut, t) -> unmark_type t) lbls
+  end;
+  begin match decl.type_manifest with
+    None    -> ()
+  | Some ty -> unmark_type ty
+  end
+
+let unmark_class_signature sign =
+  unmark_type sign.cty_self;
+  Vars.iter (fun l (m, t) -> unmark_type t) sign.cty_vars
+
+let rec unmark_class_type =
+  function
+    Tcty_constr (p, tyl, cty) ->
+      List.iter unmark_type tyl; unmark_class_type cty
+  | Tcty_signature sign ->
+      unmark_class_signature sign
+  | Tcty_fun (ty, cty) ->
+      unmark_type ty; unmark_class_type cty
+
+
 
                   (*******************************************)
                   (*  Memorization of abbreviation expansion *)
@@ -99,7 +138,22 @@ let cleanup_abbrev () =
   List.iter (fun abbr -> abbr := Mnil) !memo;
   memo := []
 
-let memorize_abbrev mem path v =
+let memorize_abbrev mem path v v' =
         (* Memorize the expansion of an abbreviation. *)
-  mem := Mcons (path, v, !mem);
+  mem := Mcons (path, v, v', !mem);
   memo := mem :: !memo
+
+let rec forget_abbrev_rec mem path =
+  match mem with
+    Mnil ->
+      assert false
+  | Mcons (path', _, _, rem) when Path.same path path' ->
+      rem 
+  | Mcons (path, v, v', rem) ->
+      Mcons (path, v, v', forget_abbrev_rec rem path)
+  | Mlink mem' ->
+      mem' := forget_abbrev_rec !mem' path;
+      raise Exit
+
+let forget_abbrev mem path =
+  try mem := forget_abbrev_rec !mem path with Exit -> ()
diff --git a/typing/btype.mli b/typing/btype.mli
index 2fcf24f04e..4a1e23b599 100644
--- a/typing/btype.mli
+++ b/typing/btype.mli
@@ -45,7 +45,12 @@ val lowest_level: int
         (* Marked type: ty.level < lowest_level *)
 val pivot_level: int
         (* Type marking: ty.level <- pivot_level - ty.level *)
+val mark_type: type_expr -> unit
+        (* Mark a type *)
 val unmark_type: type_expr -> unit
+val unmark_type_decl: type_declaration -> unit
+val unmark_class_type: class_type -> unit
+val unmark_class_signature: class_signature -> unit
         (* Remove marks from a type *)
 
 (**** Memorization of abbreviation expansion ****)
@@ -55,5 +60,8 @@ val cleanup_abbrev: unit -> unit
            When some types are saved (using [output_value]), this
            function MUST be called just before. *)
 val memorize_abbrev:
-        abbrev_memo ref -> Path.t -> type_expr -> unit
+        abbrev_memo ref -> Path.t -> type_expr -> type_expr -> unit
         (* Add an expansion in the cache *)
+val forget_abbrev:
+        abbrev_memo ref -> Path.t -> unit
+        (* Remove an abbreviation from the cache *)
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 6e4a2f1e40..3ba16e1813 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -95,24 +95,48 @@ exception Recursive_abbrev
 (**** Type level management ****)
 
 let current_level = ref 0
+let nongen_level = ref 0
 let global_level = ref 1
-
-let init_def level = current_level := level
-let begin_def () = incr current_level
-let end_def () = decr current_level
+let saved_level = ref []
+let saved_global_level = ref []
+
+let init_def level = current_level := level; nongen_level := level
+let begin_def () =
+  saved_level := (!current_level, !nongen_level) :: !saved_level;
+  incr current_level; nongen_level := !current_level
+let begin_class_def () =
+  saved_level := (!current_level, !nongen_level) :: !saved_level;
+  incr current_level
+let raise_nongen_level () =
+  saved_level := (!current_level, !nongen_level) :: !saved_level;
+  nongen_level := !current_level
+let end_def () =
+  let (cl, nl) = List.hd !saved_level in
+  saved_level := List.tl !saved_level;
+  current_level := cl; nongen_level := nl
 
 let reset_global_level () =
-  global_level := !current_level + 1
+  global_level := !current_level + 1;
+  saved_global_level := []
+let increase_global_level () =
+  saved_global_level := !global_level :: !saved_global_level;
+  global_level := !current_level
+let restore_global_level () =
+  match !saved_global_level with
+    gl::rem -> global_level := gl; saved_global_level := rem
+  | []      -> assert false
 
 (**** Some type creators ****)
 
 (* Re-export generic type creators *)
 
 let newty desc         = { desc = desc; level = !current_level }
+let newty2 level desc  = { desc = desc; level = level }
 let newgenty           = newgenty
 let new_global_ty desc = { desc = desc; level = !global_level }
 
 let newvar ()          = { desc = Tvar; level = !current_level }
+let newvar2 level      = { desc = Tvar; level = level }
 let newmarkedvar () = { desc = Tvar; level = pivot_level - !current_level }
 let newgenvar          = newgenvar
 let new_global_var ()  = new_global_ty Tvar
@@ -120,6 +144,8 @@ let newmarkedgenvar    = newmarkedgenvar
 
 let newobj fields      = newty (Tobject (fields, ref None))
 
+let newconstr path tyl = newty (Tconstr (path, tyl, ref Mnil))
+
 let none = newty (Ttuple [])                (* Clearly ill-formed type *)
 
 (**** Representative of a type ****)
@@ -134,25 +160,27 @@ let repr = repr
 
 (**** Object field manipulation. ****)
 
+let object_fields ty =
+  match (repr ty).desc with
+    Tobject (fields, _) -> fields
+  | _                   -> assert false
+
 let flatten_fields ty =
   let rec flatten l ty =
     let ty = repr ty in
     match ty.desc with
-      Tfield(s, kind, ty1, ty2) ->
-        begin match field_kind_repr kind with
-          Fabsent ->
-            flatten l ty2
-        | k ->
-            flatten ((s, k, ty1)::l) ty2
-        end
+      Tfield(s, k, ty1, ty2) ->
+        flatten ((s, k, ty1)::l) ty2
     | _ ->
         (l, ty)
   in
     let (l, r) = flatten [] ty in
-      (List.rev l, r)
+    (Sort.list (fun (n, _, _) (n', _, _) -> n < n') l, r)
 
-let build_fields =
-  List.fold_right (fun (s, k, ty1) ty2 -> newty (Tfield(s, k, ty1, ty2)))
+(* XXX Doit preserver les niveaux... *)
+let build_fields level =
+  List.fold_right
+    (fun (s, k, ty1) ty2 -> newty2 level (Tfield(s, k, ty1, ty2)))
 
 let associate_fields fields1 fields2 =
   let rec associate p s s' =
@@ -162,13 +190,13 @@ let associate_fields fields1 fields2 =
     | ([], l') ->
         (List.rev p, List.rev s, (List.rev s') @ l')
     | ((n, k, t)::r, (n', k', t')::r') when n = n' ->
-        associate ((k, t, k', t')::p) s s' (r, r')
+        associate ((n, k, t, k', t')::p) s s' (r, r')
     | ((n, k, t)::r, ((n', k', t')::_ as l')) when n < n' ->
         associate p ((n, k, t)::s) s' (r, l')
     | (((n, k, t)::r as l), (n', k', t')::r') (* when n > n' *) ->
         associate p s ((n', k', t')::s') (l, r')
-  in let sort = Sort.list (fun (n, _, _) (n', _, _) -> n < n') in
-  associate [] [] [] (sort fields1, sort fields2)
+  in
+  associate [] [] [] (fields1, fields2)
 
 (**** Check whether an object is open ****)
 
@@ -187,45 +215,40 @@ let close_object ty =
     let ty = repr ty in
     match ty.desc with
       Tvar                 -> ty.desc <- Tlink {desc = Tnil; level = ty.level}
-    | Tfield(_, k, _, ty') ->
-       close ty';
-       let k = field_kind_repr k in
-       begin match k with
-         Fvar r -> r := Some Fabsent
-       | _      -> ()
-       end
-    | Tnil                 -> ()
-    | _                    -> fatal_error "Ctype.close_object (1)"
+    | Tfield(_, _, _, ty') -> close ty'
+    | _                    -> assert false
   in
   match (repr ty).desc with
     Tobject (ty, _)   -> close ty
-  | Tconstr (_, _, _) -> ()             (* Already closed *)
-  | _                 -> fatal_error "Ctype.close_object (2)"
+  | _                 -> assert false
+
+(**** Row variable of an object type ****)
 
+let row_variable ty =
+  let rec find ty =
+    let ty = repr ty in
+    match ty.desc with
+      Tfield (_, _, _, ty) -> find ty
+    | Tvar                 -> ty
+    | _                    -> assert false
+  in
+  match (repr ty).desc with
+    Tobject (fi, _) -> find fi
+  | _               -> assert false
 
 (**** Object name manipulation ****)
 (* +++ Bientot obsolete *)
 
-let rec row_variable ty =
-  let ty = repr ty in
-  match ty.desc with
-    Tfield (_, _, _, ty) -> row_variable ty
-  | Tvar                 -> ty
-  | Tnil                 -> raise Not_found
-  | _                    -> fatal_error "Ctype.row_variable"
-
-let set_object_name ty params id =
+let set_object_name id rv params ty =
   match (repr ty).desc with
     Tobject (fi, nm) ->
       begin try
-        nm := Some (Path.Pident id, (row_variable fi)::params)
+        nm := Some (Path.Pident id, rv::params)
       with Not_found ->
         ()
       end
-  | Tconstr (_, _, _) ->
-      ()
   | _ ->
-      fatal_error "Ctype.set_object_name"
+      assert false
 
 let remove_object_name ty =
   match (repr ty).desc with
@@ -236,19 +259,183 @@ let remove_object_name ty =
 (**** Hiding of private methods ****)
 
 let hide_private_methods ty =
+  let (fl, _) = flatten_fields (object_fields ty) in
+  List.iter
+    (function (_, k, _) ->
+       let k = field_kind_repr k in
+       match k with
+         Fvar r -> r := Some Fabsent
+       | _      -> ())
+    fl
+
+
+                              (*******************************)
+                              (*  Operations on class types  *)
+                              (*******************************)
+
+
+let rec signature_of_class_type =
+  function
+    Tcty_constr (_, _, cty) -> signature_of_class_type cty
+  | Tcty_signature sign     -> sign
+  | Tcty_fun (ty, cty)      -> signature_of_class_type cty
+
+let self_type cty =
+  repr (signature_of_class_type cty).cty_self
+
+let rec class_type_arity =
+  function
+    Tcty_constr (_, _, cty) ->  class_type_arity cty
+  | Tcty_signature _        ->  0
+  | Tcty_fun (_, cty)       ->  1 + class_type_arity cty
+
+
+                    (**************************************)
+                    (*  Check genericity of type schemes  *)
+                    (**************************************)
+
+
+exception Non_closed
+
+let rec closed_schema_rec ty =
   let ty = repr ty in
-  match ty.desc with
-    Tobject (f, _) ->
-      let (fl, _) = flatten_fields f in
-      List.iter
-        (function (_, k, _) ->
-           let k = field_kind_repr k in
-           match k with
-             Fvar r -> r := Some Fabsent
-           | _      -> ())
-        fl
-  | _ ->
-      ()
+  if ty.level >= lowest_level then begin
+    let level = ty.level in
+    ty.level <- pivot_level - level;
+    match ty.desc with
+      Tvar when level <> generic_level ->
+        raise Non_closed
+    | Tobject(f, {contents = Some (_, p)}) ->
+        closed_schema_rec f;
+        List.iter closed_schema_rec p
+    | Tobject(f, _) ->
+        closed_schema_rec f
+    | Tfield(_, kind, t1, t2) ->
+        if field_kind_repr kind = Fpresent then
+          closed_schema_rec t1;
+        closed_schema_rec t2
+    | _ ->
+        iter_type_expr closed_schema_rec ty
+  end
+
+(* Return whether all variables of type [ty] are generic. *)
+let closed_schema ty =
+  try
+    closed_schema_rec ty;
+    unmark_type ty;
+    true
+  with Non_closed ->
+    unmark_type ty;
+    false
+
+exception Non_closed of type_expr
+
+let free_variables = ref []
+
+let rec free_vars_rec ty =
+  let ty = repr ty in
+  if ty.level >= lowest_level then begin
+    begin match ty.desc with
+      Tvar -> free_variables := ty :: !free_variables
+    | _    -> ()
+    end;
+    ty.level <- pivot_level - ty.level;
+    iter_type_expr free_vars_rec ty
+  end
+
+let free_vars ty =
+  free_variables := [];
+  free_vars_rec ty;
+  let res = !free_variables in
+  free_variables := [];
+  res
+
+let rec closed_type ty =
+  match free_vars ty with
+      []   -> ()
+  | v :: _ -> raise (Non_closed v)
+
+let closed_parameterized_type params ty =
+  List.iter mark_type params;
+  try
+    closed_type ty;
+    List.iter unmark_type params;
+    unmark_type ty;
+    true
+  with Non_closed _ ->
+    List.iter unmark_type params;
+    unmark_type ty;
+    false
+
+let closed_type_decl decl =
+  try
+    List.iter mark_type decl.type_params;
+    begin match decl.type_kind with
+      Type_abstract ->
+        ()
+    | Type_variant v ->
+        List.iter (fun (_, tyl) -> List.iter closed_type tyl) v
+    | Type_record r ->
+        List.iter (fun (_, _, ty) -> closed_type ty) r
+    end;
+    begin match decl.type_manifest with
+      None    -> ()
+    | Some ty -> closed_type ty
+    end;
+    unmark_type_decl decl;
+    None
+  with Non_closed ty ->
+    unmark_type_decl decl;
+    Some ty
+
+type closed_class_failure =
+    CC_Method of type_expr * string * type_expr
+  | CC_Value of type_expr * string * type_expr
+
+exception Failure of closed_class_failure
+
+let closed_class params sign =
+  let ty = object_fields (repr sign.cty_self) in
+  let (fields, rest) = flatten_fields ty in
+  List.iter mark_type params;
+  mark_type rest;
+  List.iter
+    (fun (lab, _, ty) -> if lab = "*dummy method*" then mark_type ty)
+    fields;
+  try
+    List.iter
+      (fun (lab, _, ty) ->
+        try closed_type ty with Non_closed ty0 ->
+          raise (Failure (CC_Method (ty0, lab, ty))))
+      fields;
+    Vars.iter
+      (fun lab (_, ty) ->
+        try closed_type ty with Non_closed ty0 ->
+          raise (Failure (CC_Value (ty0, lab, ty))))
+      sign.cty_vars;
+    mark_type sign.cty_self;
+    List.iter unmark_type params;
+    unmark_class_signature sign;
+    None
+  with Failure reason ->
+    mark_type sign.cty_self;
+    List.iter unmark_type params;
+    unmark_class_signature sign;
+    Some reason
+
+
+                            (**********************)
+                            (*  Type duplication  *)
+                            (**********************)
+
+
+(* Duplicate a type, preserving only type variables *)
+let duplicate_type ty =
+  Subst.type_expr Subst.identity ty
+
+(* Same, for class types *)
+let duplicate_class_type ty =
+  Subst.class_type Subst.identity ty
 
 
                          (*****************************)
@@ -262,23 +449,36 @@ let hide_private_methods ty =
    [expand_abbrev] (via [subst]) requires these expansions to be
    preserved. Does it worth duplicating this code ?
 *)
-let rec generalize ty =
+let rec iter_generalize tyl ty =
   let ty = repr ty in
   if (ty.level > !current_level) && (ty.level <> generic_level) then begin
     ty.level <- generic_level;
     begin match ty.desc with
       Tconstr (_, _, abbrev) ->
-        generalize_expans !abbrev
+        generalize_expans tyl !abbrev
     | _ -> ()
     end;
-    iter_type_expr generalize ty
-  end
+    iter_type_expr (iter_generalize tyl) ty
+  end else
+    tyl := ty :: !tyl
 
-and generalize_expans =
+and generalize_expans tyl =
   function
-    Mnil              ->  ()
-  | Mcons(_, ty, rem) ->  generalize ty; generalize_expans rem
-  | Mlink rem         ->  generalize_expans !rem
+    Mnil                   -> ()
+  | Mcons(_, ty, ty', rem) -> iter_generalize tyl ty;
+                              iter_generalize tyl ty';
+                              generalize_expans tyl rem
+  | Mlink rem              -> generalize_expans tyl !rem
+
+let rec generalize ty =
+  iter_generalize (ref []) ty
+
+(* Efficient repeated generalisation of the same type *)
+let iterative_generalization min_level tyl =
+  let tyl' = ref [] in
+  List.iter (iter_generalize tyl') tyl;
+  List.fold_right (fun ty l -> if ty.level <= min_level then l else ty::l)
+    !tyl' []
 
 let try_expand_head' = (* Forward declaration *)
   ref (fun env ty -> raise Cannot_expand)
@@ -306,8 +506,15 @@ let rec update_level env level ty =
           update_level env level ty
         with Cannot_expand ->
           (* +++ Levels should be restored... *)
-          raise (Unify [])
+          raise (Unify [(ty, newvar2 level)])
         end
+    | Tfield(_, k, _, _) ->
+        begin match field_kind_repr k with
+          Fvar _ (* {contents = None} *) -> raise (Unify [(ty, newvar2 level)])
+        | _                              -> ()
+        end;
+        ty.level <- level;
+        iter_type_expr (update_level env level) ty
     | _ ->
         ty.level <- level;
         iter_type_expr (update_level env level) ty
@@ -320,11 +527,55 @@ let rec update_level env level ty =
    type constructor path). So, it can be called with the empty
    environnement.
 *)
-let make_nongen ty = update_level Env.empty !current_level ty
+let make_nongen ty =
+  try
+    update_level Env.empty !nongen_level ty
+  with Unify [_, ty'] ->
+    raise (Unify [ty, ty'])
 
 (* Correct the levels of type [ty]. *)
 let correct_levels ty =
-  Subst.type_expr Subst.identity ty
+  duplicate_type ty
+
+(* Only generalize the type ty0 in ty *)
+let limited_generalize ty0 ty =
+  let ty0 = repr ty0 in
+
+  let graph = Hashtbl.create 17 in
+  let idx = ref lowest_level in
+  let roots = ref [] in
+
+  let rec inverse pty ty =
+    let ty = repr ty in
+    if (ty.level > !current_level) || (ty.level = generic_level) then begin
+      decr idx;
+      Hashtbl.add graph !idx (ty, ref pty);
+      if (ty.level = generic_level) || (ty == ty0) then
+        roots := ty :: !roots;
+      ty.level <- !idx;
+      iter_type_expr (inverse [ty]) ty
+    end else if ty.level < lowest_level then begin
+      let (_, parents) = Hashtbl.find graph ty.level in
+      parents := pty @ !parents
+    end
+
+  and generalize_parents ty =
+    let idx = ty.level in
+    if idx <> generic_level then begin
+      ty.level <- generic_level;
+      List.iter generalize_parents !(snd (Hashtbl.find graph idx))
+    end
+  in
+
+  inverse [] ty;
+  if ty0.level < lowest_level then
+    iter_type_expr (inverse []) ty0;
+  List.iter generalize_parents !roots;
+  Hashtbl.iter
+    (fun _ (ty, _) ->
+       if ty.level <> generic_level then
+         ty.level <- !current_level)
+    graph
 
 
                               (*******************)
@@ -332,6 +583,17 @@ let correct_levels ty =
                               (*******************)
 
 
+let rec find_repr p1 =
+  function
+    Mnil ->
+      None
+  | Mcons (p2, ty, _, _) when Path.same p1 p2 ->
+      Some ty
+  | Mcons (_, _, _, rem) ->
+      find_repr p1 rem
+  | Mlink {contents = rem} ->
+      find_repr p1 rem
+
 (*
    Generic nodes are duplicated, while non-generic nodes are left
    as-is.
@@ -364,6 +626,10 @@ let rec copy ty =
       | Ttuple tl ->
           Ttuple (List.map copy tl)
       | Tconstr (p, tl, _) ->
+          begin match find_repr p !(!abbreviations) with
+            Some ty when repr ty != t -> (* XXX Commentaire *)
+              Tlink ty
+          | _ ->
           (*
              One must allocate a new reference, so that abbrevia-
              tions belonging to different branches of a type are
@@ -373,10 +639,11 @@ let rec copy ty =
              ation can be released by changing the content of just
              one reference.
           *)
-          Tconstr (p, List.map copy tl,
-                   ref (match ! !abbreviations with
-                          Mcons _ -> Mlink !abbreviations
-                        | abbrev  -> abbrev))
+              Tconstr (p, List.map copy tl,
+                       ref (match !(!abbreviations) with
+                              Mcons _ -> Mlink !abbreviations
+                            | abbrev  -> abbrev))
+          end
       | Tobject (t1, {contents = name}) ->
           let name' =
             match name with
@@ -390,8 +657,10 @@ let rec copy ty =
           begin match field_kind_repr kind with
             Fpresent ->
               Tfield (label, Fpresent, copy t1, copy t2)
-          | _ ->
-              Tlink (copy t2)
+          | Fvar _ (* {contents = None} *) ->
+              Tfield (label, Fvar (ref None), copy t1, copy t2)
+          | Fabsent ->
+              assert false
           end
       | Tnil ->
           Tnil
@@ -445,32 +714,54 @@ let instance_parameterized_type_2 sch_args sch_lst sch =
   unmark_type ty;  
   (ty_args, ty_lst, ty)
 
-let instance_class cl =
-  let params = List.map copy cl.cty_params in
-  let args = List.map copy cl.cty_args in
-  let vars = Vars.map (function (mut, ty) -> (mut, copy ty)) cl.cty_vars in
-  let mets = Meths.map copy cl.cty_meths in
-  let self = copy cl.cty_self in
+let instance_class params cty =
+  let rec copy_class_type =
+    function
+      Tcty_constr (path, tyl, cty) ->
+        Tcty_constr (path, List.map copy tyl, copy_class_type cty)
+    | Tcty_signature sign ->
+        Tcty_signature
+          {cty_self = copy sign.cty_self;
+           cty_vars =
+             Vars.map (function (mut, ty) -> (mut, copy ty)) sign.cty_vars;
+           cty_concr = sign.cty_concr}
+    | Tcty_fun (ty, cty) ->
+        Tcty_fun (copy ty, copy_class_type cty)
+  in
+  let params' = List.map copy params in
+  let cty' = copy_class_type cty in
   cleanup_types ();
-  List.iter unmark_type params; List.iter unmark_type args;
-  Vars.iter (fun l (m, t) -> unmark_type t) vars;
-  Meths.iter (fun l t -> unmark_type t) mets;
-  unmark_type self;
-  (params, args, vars, mets, self)
+  let rec unmark_class_type =
+    function
+      Tcty_constr (path, tyl, cty) ->
+        List.iter unmark_type tyl;
+        unmark_class_type cty
+    | Tcty_signature sign ->
+        unmark_type sign.cty_self;
+        Vars.iter (fun lab (mut, ty) -> unmark_type ty) sign.cty_vars;
+    | Tcty_fun (ty, cty) ->
+        unmark_type ty; unmark_class_type cty
+  in
+  List.iter unmark_type params';
+  unmark_class_type cty';
+  (params', cty')
 
 (**** Instantiation with parameter substitution ****)
 
 let unify' = (* Forward declaration *)
   ref (fun env ty1 ty2 -> raise (Unify []))
 
-let rec subst env level abbrev path params args body =
+let rec subst env level abbrev ty params args body =
   let old_level = !current_level in
   current_level := level;
   try
     let body0 = newvar () in          (* Stub *)
-    begin match path with
+    begin match ty with
       None      -> ()
-    | Some path -> memorize_abbrev abbrev path body0
+    | Some ({desc = Tconstr (path, _, _)} as ty) ->
+        memorize_abbrev abbrev path ty body0
+    | _ ->
+        assert false
     end;
     abbreviations := abbrev;
     let (params', body') = instance_parameterized_type params body in
@@ -506,9 +797,9 @@ let rec find_expans p1 =
   function
     Mnil ->
       None
-  | Mcons (p2, ty, _) when Path.same p1 p2 ->
+  | Mcons (p2, _, ty, _) when Path.same p1 p2 ->
       Some ty
-  | Mcons (_, _, rem) ->
+  | Mcons (_, _, _, rem) ->
       find_expans p1 rem
   | Mlink {contents = rem} ->
       find_expans p1 rem
@@ -533,39 +824,45 @@ let previous_env = ref Env.empty
    4. The expansion requires the expansion of another abbreviation,
       and this other expansion fails.
 *)
-let expand_abbrev env path args abbrev level =
+let expand_abbrev env ty =
   (* 
      If the environnement has changed, memorized expansions might not
      be correct anymore, and so we flush the cache. This is safe but
-     quite pessimistic: it would be enough to flush the cache at the
-     ends of structures and signatures.
-     +++ Do it !
+     quite pessimistic: it would be enough to flush the cache when a
+     type or module definition is overriden in the environnement.
   *)
   if env != !previous_env then begin
     cleanup_abbrev ();
     previous_env := env
   end;
-  match find_expans path !abbrev with
-    Some ty ->
-      if level <> generic_level then
-        update_level env level ty;
-      ty
-  | None ->
-      let (params, body) =
-        try Env.find_type_expansion path env with Not_found ->
-          raise Cannot_expand
-      in
-      try
-        subst env level abbrev (Some path) params args body
-      with Unify _ -> raise Cannot_expand
+  match ty with
+    {desc = Tconstr (path, args, abbrev); level = level} ->
+      begin match find_expans path !abbrev with
+        Some ty ->
+          if level <> generic_level then
+            update_level env level ty;
+          ty
+      | None ->
+          let (params, body) =
+            try Env.find_type_expansion path env with Not_found ->
+              raise Cannot_expand
+          in
+          begin try
+            subst env level abbrev (Some ty) params args body
+          with Unify _ ->
+            raise Cannot_expand
+          end
+      end
+  | _ ->
+      assert false
 
 (* Fully expand the head of a type. Raise an exception if the type
    cannot be expanded. *)
 let rec try_expand_head env ty =
   let ty = repr ty in
   match ty.desc with
-    Tconstr(p, tl, abbrev) ->
-      let ty' = expand_abbrev env p tl abbrev ty.level in
+    Tconstr _ ->
+      let ty' = expand_abbrev env ty in
       begin try
         try_expand_head env ty'
       with Cannot_expand ->
@@ -636,7 +933,8 @@ let rec non_recursive_abbrev env ty =
 let correct_abbrev env ident params ty =
   visited := [];
   non_recursive_abbrev env
-    (subst env generic_level (ref (Mcons (Path.Pident ident, none, Mnil))) None
+    (subst env generic_level
+       (ref (Mcons (Path.Pident ident, none, none, Mnil))) None
        [] [] ty);
   visited := []
 
@@ -676,16 +974,6 @@ let expand_trace env trace =
        (repr t1, full_expand env t1)::(repr t2, full_expand env t2)::rem)
     trace []
 
-let rec filter_trace =
-  function
-    (t1, t1')::(t2, t2')::rem ->
-      let rem' = filter_trace rem in
-      if (t1 == t1') & (t2 == t2')
-      then rem'
-      else (t1, t1')::(t2, t2')::rem'
-  | _ ->
-      []
-
 (**** Unification ****)
 
 (* Return whether [t0] occurs in [ty]. Objects are also traversed. *)
@@ -775,16 +1063,10 @@ and unify3 env t1 t1' t2 t2' =
   (* Assumes either [t1 == t1'] or [t2 != t2'] *)
   let d1 = t1'.desc and d2 = t2'.desc in
   
-  if (t2 != t2') && (deep_occur t1' t2) then begin
-    (* See point 3. *)
-    occur env t1' t2';
-    update_level env t1'.level t2';
-    t1'.desc <- Tlink t2'
-  end else begin
-    occur env t1' t2;
-    update_level env t1'.level t2;
-    t1'.desc <- Tlink t2
-  end;
+  let create_recursion = (t2 != t2') && (deep_occur t1' t2) in
+  occur env t1' t2;
+  update_level env t1'.level t2;
+  t1'.desc <- Tlink t2;
 
   try
     begin match (d1, d2) with
@@ -823,17 +1105,24 @@ and unify3 env t1 t1' t2 t2' =
         end
     | (Tfield _, Tfield _) ->           (* Actually unused *)
         unify_fields env t1' t2'
-    | (Tfield (_, kind, _, t1''), _) ->
-        unify_kind kind Fabsent;
-        unify env t1'' t2'
-    | (_, Tfield (_, kind, _, t2'')) ->
-        unify_kind kind Fabsent;
-        unify env t1' t2''
     | (Tnil, Tnil) ->
         ()
     | (_, _) ->
         raise (Unify [])
+    end;
+
+(* XXX Commentaires + changer "create_recursion" *)
+    if create_recursion then begin
+      match t2.desc with
+        Tconstr (p, tl, abbrev) ->
+          forget_abbrev abbrev p;
+          let t2'' = expand_head env t2 in
+          if not (closed_parameterized_type tl t2'') then
+            (repr t2).desc <- Tlink (repr t2')
+      | _ ->
+          assert false
     end
+
 (*
     (* 
        Can only be done afterwards, once the row variable has
@@ -872,29 +1161,30 @@ and unify_fields env ty1 ty2 =          (* Optimization *)
   and (fields2, rest2) = flatten_fields ty2 in
   let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
   let va = newvar () in
-  unify env rest1 (build_fields miss2 va);
-  unify env (build_fields miss1 va) rest2;
-  List.iter (fun (k1, t1, k2, t2) -> unify_kind k1 k2; unify env t1 t2) pairs
+  unify env (build_fields ty1.level miss1 va) rest2;
+  unify env rest1 (build_fields ty2.level miss2 va);
+  List.iter
+    (fun (n, k1, t1, k2, t2) ->
+       unify_kind k1 k2;
+       try unify env t1 t2 with Unify trace ->
+         raise (Unify ((newty (Tfield(n, k1, t1, va)),
+                        newty (Tfield(n, k2, t2, va)))::trace)))
+    pairs
 
 and unify_kind k1 k2 =
   let k1 = field_kind_repr k1 in
   let k2 = field_kind_repr k2 in
   match k1, k2 with
-    (Fvar r, _)                               -> r := Some k2
-  | (_, Fvar r)                               -> r := Some k1
-  | (Fabsent, Fabsent) | (Fpresent, Fpresent) -> ()
-  | _                                         -> raise (Unify [])
+    (Fvar r, (Fvar _ | Fpresent))             -> r := Some k2
+  | (Fpresent, Fvar r)                        -> r := Some k1
+  | (Fpresent, Fpresent)                      -> ()
+  | _                                         -> assert false
 
 let unify env ty1 ty2 =
   try
     unify env ty1 ty2
   with Unify trace ->
-    let trace = expand_trace env trace in
-    match trace with
-      t1::t2::rem ->
-        raise (Unify (t1::t2::filter_trace rem))
-    | _ ->
-        fatal_error "Ctype.unify"
+    raise (Unify (expand_trace env trace))
 
 let _ = unify' := unify
 
@@ -920,15 +1210,15 @@ let rec filter_method_field env name priv ty =
   let ty = repr ty in
   match ty.desc with
     Tvar ->
-      let ty1 = newvar () and ty2 = newvar () in
-      let ty' = newty (Tfield (name,
-                               begin match priv with
-                                 Private -> Fvar (ref None)
-                               | Public  -> Fpresent
-                               end,
-                               ty1, ty2))
+      let level = ty.level in
+      let ty1 = newvar2 level and ty2 = newvar2 level in
+      let ty' = newty2 level (Tfield (name,
+                                      begin match priv with
+                                        Private -> Fvar (ref None)
+                                      | Public  -> Fpresent
+                                      end,
+                                      ty1, ty2))
       in
-      update_level env ty.level ty';
       ty.desc <- Tlink ty';
       ty1
   | Tfield(n, kind, ty1, ty2) ->
@@ -939,8 +1229,6 @@ let rec filter_method_field env name priv ty =
         ty1
       end else
         filter_method_field env name priv ty2
-  | _ when priv = Private ->
-      newvar ()
   | _ ->
       raise (Unify [])
 
@@ -959,6 +1247,15 @@ let rec filter_method env name priv ty =
   | _ ->
       raise (Unify [])
 
+let filter_self_method env lab priv meths ty =
+  let ty' = filter_method env lab priv ty in
+  try
+    Meths.find lab !meths
+  with Not_found ->
+    let pair = (Ident.create lab, ty') in
+    meths := Meths.add lab pair !meths;
+    pair
+
 
                         (***********************************)
                         (*  Matching between type schemes  *)
@@ -984,22 +1281,13 @@ let moregen_occur env level ty =
   end;
   update_level env level ty
 
-(*
-   Non-generic variable can be instanciated only if [inst_nongen] is
-   true. So, [inst_nongen] should be set to false if the subject might
-   contain non-generic variables.
-   Usually, the subject is given by the user, and the pattern
-   is unimportant.  So, no need to propagate abbreviations.
-*)
-let moregeneral env inst_nongen pat_sch subj_sch =
-  let type_pairs = ref [] in
-
-  let rec moregen env t1 t2 =
-    if t1 == t2 then () else
-    let t1 = repr t1 in
-    let t2 = repr t2 in
-    if t1 == t2 then () else
+let rec moregen inst_nongen type_pairs env t1 t2 =
+  if t1 == t2 then () else
+  let t1 = repr t1 in
+  let t2 = repr t2 in
+  if t1 == t2 then () else
 
+  try
     match (t1.desc, t2.desc) with
       (Tvar, _) when if inst_nongen then t1.level <> generic_level - 1
                                     else t1.level =  generic_level ->
@@ -1014,10 +1302,9 @@ let moregeneral env inst_nongen pat_sch subj_sch =
         let t1' = repr t1' and t2' = repr t2' in
         if t1' == t2' then () else
         if
-          List.exists (function (t1, t2) -> t1 == t1' && t2 == t2') !type_pairs
-        then
-          ()
-        else begin
+          List.exists (function (t1, t2) -> t1 == t1' && t2 == t2')
+            !type_pairs
+        then () else begin
           type_pairs := (t1', t2') :: !type_pairs;
 
           match (t1'.desc, t2'.desc) with
@@ -1026,65 +1313,84 @@ let moregeneral env inst_nongen pat_sch subj_sch =
               moregen_occur env t1'.level t2;
               t1'.desc <- Tlink t2
           | (Tarrow (t1, u1), Tarrow (t2, u2)) ->
-              moregen env t1 t2; moregen env u1 u2
+              moregen inst_nongen type_pairs env t1 t2;
+              moregen inst_nongen type_pairs env u1 u2
           | (Ttuple tl1, Ttuple tl2) ->
-              moregen_list env tl1 tl2
+              moregen_list inst_nongen type_pairs env tl1 tl2
           | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _))
                 when Path.same p1 p2 ->
-              moregen_list env tl1 tl2
+              moregen_list inst_nongen type_pairs env tl1 tl2
           | (Tobject (fi1, nm1), Tobject (fi2, nm2)) ->
-              moregen_fields env fi1 fi2
+              moregen_fields inst_nongen type_pairs env fi1 fi2
           | (Tfield _, Tfield _) ->           (* Actually unused *)
-              moregen_fields env t1' t2'
-          | (Tfield (_, kind, _, t1''), _) ->
-              moregen_kind kind Fabsent;
-              moregen env t1'' t2'
-          | (_, Tfield (_, kind, _, t2'')) ->
-              moregen_kind Fabsent kind;
-              moregen env t1' t2''
+              moregen_fields inst_nongen type_pairs env t1' t2'
+          | (Tfield (_, kind, _, t1''), _)
+                when field_kind_repr kind = Fabsent ->
+              moregen inst_nongen type_pairs env t1'' t2'
+          | (_, Tfield (_, kind, _, t2''))
+                when field_kind_repr kind = Fabsent ->
+              moregen inst_nongen type_pairs env t1' t2''
           | (Tnil, Tnil) ->
               ()
           | (_, _) ->
               raise (Unify [])
         end
+  with Unify trace ->
+    raise (Unify ((t1, t2)::trace))
 
-  and moregen_list env tl1 tl2 =
-    if List.length tl1 <> List.length tl2 then
-      raise (Unify []);
-    List.iter2 (moregen env) tl1 tl2
-
-  and moregen_fields env ty1 ty2 =
-    let (fields1, rest1) = flatten_fields ty1
-    and (fields2, rest2) = flatten_fields ty2 in
-    let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
-    if miss1 <> [] then raise (Unify []);
-    moregen env rest1 (build_fields miss2 rest2);
-    List.iter
-      (fun (k1, t1, k2, t2) -> moregen_kind k1 k2; moregen env t1 t2)
-      pairs
+and moregen_list inst_nongen type_pairs env tl1 tl2 =
+  if List.length tl1 <> List.length tl2 then
+    raise (Unify []);
+  List.iter2 (moregen inst_nongen type_pairs env) tl1 tl2
 
-  and moregen_kind level k1 k2 =
-    let k1 = field_kind_repr k1 in
-    let k2 = field_kind_repr k2 in
-    match k1, k2 with
-      (Fvar r, _)                               -> r := Some k2
-    | (Fabsent, Fabsent) | (Fpresent, Fpresent) -> ()
-    | _                                         -> raise (Unify [])
+and moregen_fields inst_nongen type_pairs env ty1 ty2 =
+  let (fields1, rest1) = flatten_fields ty1
+  and (fields2, rest2) = flatten_fields ty2 in
+  let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
+  if miss1 <> [] then raise (Unify []);
+  moregen inst_nongen type_pairs env rest1
+    (build_fields ty2.level miss2 rest2);
+  List.iter
+    (fun (n, k1, t1, k2, t2) ->
+       moregen_kind k1 k2;
+       try moregen inst_nongen type_pairs env t1 t2 with Unify trace ->
+         raise (Unify ((newty (Tfield(n, k1, t1, rest2)),
+                        newty (Tfield(n, k2, t2, rest2)))::trace)))
+    pairs
+
+and moregen_kind k1 k2 =
+  let k1 = field_kind_repr k1 in
+  let k2 = field_kind_repr k2 in
+  match k1, k2 with
+    (Fvar r, (Fvar _ | Fpresent))  -> r := Some k2
+  | (Fpresent, Fpresent)           -> ()
+  | _                              -> raise (Unify [])
 
-  in
+(*
+   Non-generic variable can be instanciated only if [inst_nongen] is
+   true. So, [inst_nongen] should be set to false if the subject might
+   contain non-generic variables (and we do not want them to be
+   instanciated).
+   Usually, the subject is given by the user, and the pattern
+   is unimportant.  So, no need to propagate abbreviations.
+*)
+let moregeneral env inst_nongen pat_sch subj_sch =
   let old_level = !current_level in
   current_level := generic_level - 1;
   (*
      Generic variables are first duplicated with [instance].  So,
      their levels are lowered to [generic_level - 1].  The subject is
-     then copied with [correct_levels].  That way, its levels won't be
+     then copied with [duplicate_type].  That way, its levels won't be
      changed.
   *)
-  let subj = correct_levels (instance subj_sch) in
+  let subj = duplicate_type (instance subj_sch) in
   current_level := generic_level;
   (* Duplicate generic variables *)
   let patt = instance pat_sch in
-  let res = try moregen env patt subj; true with Unify _ -> false in
+  let res =
+    try moregen inst_nongen (ref []) env patt subj; true with
+      Unify _ -> false
+  in
   current_level := old_level;
   res
 
@@ -1094,86 +1400,373 @@ let moregeneral env inst_nongen pat_sch subj_sch =
                  (*********************************************)
 
 
-(* Two modes: with or without renaming of variables *)
-
-let equal env rename tyl1 tyl2 =
-  let subst = ref [] in
-  let type_pairs = ref [] in
+let rec eqtype rename type_pairs subst env t1 t2 =
+  if t1 == t2 then () else
+  let t1 = repr t1 in
+  let t2 = repr t2 in
+  if t1 == t2 then () else
 
-  let rec eqtype t1 t2 =
-    if t1 == t2 then true else
-    let t1 = repr t1 in
-    let t2 = repr t2 in
-    if t1 == t2 then true else
+  try
     match (t1.desc, t2.desc) with
-    | (Tvar, Tvar) when rename ->
+      (Tvar, Tvar) when rename ->
         begin try
-          List.assq t1 !subst == t2
+          if List.assq t1 !subst != t2 then raise (Unify [])
         with Not_found ->
-          subst := (t1, t2) :: !subst;
-          true
+          subst := (t1, t2) :: !subst
         end
     | (Tconstr (p1, [], _), Tconstr (p2, [], _)) when Path.same p1 p2 ->
-        true
+        ()
     | _ ->
-        let t1 = expand_head env t1 in
-        let t2 = expand_head env t2 in
+        let t1' = expand_head env t1 in
+        let t2' = expand_head env t2 in
         (* Expansion may have changed the representative of the types... *)
-        let t1 = repr t1 and t2 = repr t2 in
-        if t1 == t2 then true else
-        List.exists (function (t1', t2') -> t1 == t1' & t2 == t2') !type_pairs
-              (* XXX Possibly slow... *)
-          ||
-        begin
-          type_pairs := (t1, t2) :: !type_pairs;
-          match (t1.desc, t2.desc) with
+        let t1' = repr t1' and t2' = repr t2' in
+        if t1' == t2' then () else
+        if
+          List.exists (function (t1, t2) -> t1 == t1' & t2 == t2')
+            !type_pairs
+        then () else begin
+          type_pairs := (t1', t2') :: !type_pairs;
+
+          match (t1'.desc, t2'.desc) with
             (Tvar, Tvar) when rename ->
               begin try
-                List.assq t1 !subst == t2
+                if List.assq t1' !subst == t2' then raise (Unify [])
               with Not_found ->
-                subst := (t1, t2) :: !subst;
-                true
+                subst := (t1', t2') :: !subst
               end
           | (Tarrow (t1, u1), Tarrow (t2, u2)) ->
-              eqtype t1 t2 && eqtype u1 u2
+              eqtype rename type_pairs subst env t1 t2;
+              eqtype rename type_pairs subst env u1 u2;
           | (Ttuple tl1, Ttuple tl2) ->
-              eqtype_list tl1 tl2
+              eqtype_list rename type_pairs subst env tl1 tl2
           | (Tconstr (p1, tl1, _), Tconstr (p2, tl2, _))
                 when Path.same p1 p2 ->
-              eqtype_list tl1 tl2
+              eqtype_list rename type_pairs subst env tl1 tl2
           | (Tobject (fi1, nm1), Tobject (fi2, nm2)) ->
-              eqtype_fields fi1 fi2
+              eqtype_fields rename type_pairs subst env fi1 fi2
           | (Tfield _, Tfield _) ->       (* Actually unused *)
-              eqtype_fields t1 t2
-          | (Tfield (_, kind, _, t1'), _)
+              eqtype_fields rename type_pairs subst env t1' t2'
+          | (Tfield (_, kind, _, t1''), _)
                 when field_kind_repr kind = Fabsent ->
-              eqtype t1' t2
-          | (_, Tfield (_, kind, _, t2'))
+              eqtype rename type_pairs subst env t1'' t2'
+          | (_, Tfield (_, kind, _, t2''))
                 when field_kind_repr kind = Fabsent ->
-              eqtype t1 t2'
+              eqtype rename type_pairs subst env t1' t2''
           | (Tnil, Tnil) ->
-              true
+              ()
           | (_, _) ->
-              false
+              raise (Unify [])
         end
+  with Unify trace ->
+    raise (Unify ((t1, t2)::trace))
 
-  and eqtype_list tl1 tl2 =
-    List.length tl1 = List.length tl2
-                   &&
-    List.for_all2 eqtype tl1 tl2
+and eqtype_list rename type_pairs subst env tl1 tl2 =
+  if List.length tl1 <> List.length tl2 then
+    raise (Unify []);
+  List.iter2 (eqtype rename type_pairs subst env) tl1 tl2
 
-  and eqtype_fields ty1 ty2 =           (* Optimization *)
-    let (fields1, rest1) = flatten_fields ty1
-    and (fields2, rest2) = flatten_fields ty2 in
+and eqtype_fields rename type_pairs subst env ty1 ty2 =
+  let (fields1, rest1) = flatten_fields ty1
+  and (fields2, rest2) = flatten_fields ty2 in
+  let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
+  eqtype rename type_pairs subst env rest1 rest2;
+  if (miss1 <> []) || (miss2 <> []) then raise (Unify []);
+  List.iter
+    (function (n, k1, t1, k2, t2) ->
+       eqtype_kind k1 k2;
+       try eqtype rename type_pairs subst env t1 t2 with Unify trace ->
+         raise (Unify ((newty (Tfield(n, k1, t1, rest2)),
+                        newty (Tfield(n, k2, t2, rest2)))::trace)))
+    pairs
+
+and eqtype_kind k1 k2 =
+  let k1 = field_kind_repr k1 in
+  let k2 = field_kind_repr k2 in
+  match k1, k2 with
+    (Fvar _, Fvar _)
+  | (Fpresent, Fpresent) -> ()
+  | _                    -> raise (Unify [])
+
+(* Two modes: with or without renaming of variables *)
+let equal env rename tyl1 tyl2 =
+  try eqtype_list rename (ref []) (ref []) env tyl1 tyl2; true with
+    Unify _ -> false
+
+
+                          (*************************)
+                          (*  Class type matching  *)
+                          (*************************)
+
+
+type class_match_failure =
+    CM_Virtual_class
+  | CM_Parameter_arity_mismatch of int * int
+  | CM_Type_parameter_mismatch of (type_expr * type_expr) list
+  | CM_Class_type_mismatch of class_type * class_type
+  | CM_Parameter_mismatch of (type_expr * type_expr) list
+  | CM_Val_type_mismatch of string * (type_expr * type_expr) list
+  | CM_Meth_type_mismatch of string * (type_expr * type_expr) list
+  | CM_Non_mutable_value of string
+  | CM_Missing_value of string
+  | CM_Missing_method of string
+  | CM_Hide_public of string
+  | CM_Hide_virtual of string
+  | CM_Public_method of string
+  | CM_Private_method of string
+  | CM_Virtual_method of string
+
+exception Failure of class_match_failure list
+
+let rec moregen_clty trace type_pairs env cty1 cty2 =
+  try
+    match cty1, cty2 with
+      Tcty_constr (_, _, cty1), _ ->
+        moregen_clty true type_pairs env cty1 cty2
+    | _, Tcty_constr (_, _, cty2) ->
+        moregen_clty true type_pairs env cty1 cty2
+    | Tcty_fun (ty1, cty1'), Tcty_fun (ty2, cty2') ->
+        begin try moregen true type_pairs env ty1 ty2 with Unify trace ->
+          raise (Failure [CM_Parameter_mismatch (expand_trace env trace)])
+        end;
+        moregen_clty false type_pairs env cty1' cty2'
+    | Tcty_signature sign1, Tcty_signature sign2 ->
+        let ty1 = object_fields (repr sign1.cty_self) in
+        let ty2 = object_fields (repr sign2.cty_self) in
+        let (fields1, rest1) = flatten_fields ty1
+        and (fields2, rest2) = flatten_fields ty2 in
+        let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
+        List.iter
+          (fun (lab, k1, t1, k2, t2) ->
+            begin try moregen true type_pairs env t1 t2 with Unify trace ->
+              raise (Failure [CM_Meth_type_mismatch
+                                 (lab, expand_trace env trace)])
+           end)
+        pairs;
+      Vars.iter
+        (fun lab (mut, ty) ->
+           let (mut', ty') = Vars.find lab sign1.cty_vars in
+           try moregen true type_pairs env ty ty' with Unify trace ->
+             raise (Failure [CM_Val_type_mismatch
+                                (lab, expand_trace env trace)]))
+        sign2.cty_vars
+  | _ ->
+      raise (Failure [])
+  with
+    Failure error when trace ->
+      raise (Failure (CM_Class_type_mismatch (cty1, cty2)::error))
+
+let match_class_types env pat_sch subj_sch =
+  let type_pairs = ref [] in
+  let old_level = !current_level in
+  current_level := generic_level - 1;
+  (*
+     Generic variables are first duplicated with [instance].  So,
+     their levels are lowered to [generic_level - 1].  The subject is
+     then copied with [duplicate_type].  That way, its levels won't be
+     changed.
+  *)
+  let (_, subj_inst) = instance_class [] subj_sch in
+  let subj = duplicate_class_type subj_inst in
+  current_level := generic_level;
+  (* Duplicate generic variables *)
+  let (_, patt) = instance_class [] pat_sch in
+  let res =
+    let sign1 = signature_of_class_type patt in
+    let sign2 = signature_of_class_type subj in
+    let t1 = repr sign1.cty_self in
+    let t2 = repr sign2.cty_self in
+    type_pairs := (t1, t2) :: !type_pairs;
+    let (fields1, rest1) = flatten_fields (object_fields t1)
+    and (fields2, rest2) = flatten_fields (object_fields t2) in
     let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
-    eqtype rest1 rest2
-      &&
-    (miss1 = []) && (miss2 = [])
-      &&
-    List.for_all (function (k1, t1, k2, t2) -> eqtype t1 t2) pairs
+    let error =
+      List.fold_right
+        (fun (lab, k, _) err ->
+           let err =
+             let k = field_kind_repr k in
+             begin match k with
+               Fvar r -> r := Some Fabsent; err
+             | _      ->                    CM_Hide_public lab::err
+             end
+           in
+           if Concr.mem lab sign1.cty_concr then err
+           else CM_Hide_virtual lab::err)
+        miss1 []
+    in
+    let missing_method = List.map (fun (m, _, _) -> m) miss2 in
+    let error =
+      (List.map (fun m -> CM_Missing_method m) missing_method) @ error
+    in
+    (* Always succeeds *)
+    moregen true type_pairs env rest1 rest2;
+    let error =
+      List.fold_right
+        (fun (lab, k1, t1, k2, t2) err ->
+           try moregen_kind k1 k2; err with
+             Unify _ -> CM_Public_method lab::err)
+        pairs error
+    in
+    let error =
+      Vars.fold
+        (fun lab (mut, ty) err ->
+          try
+            let (mut', ty') = Vars.find lab sign1.cty_vars in
+            if mut = Mutable && mut' <> Mutable then
+              CM_Non_mutable_value lab::err
+            else
+              err
+          with Not_found ->
+            CM_Missing_value lab::err)
+        sign2.cty_vars error
+    in
+    let error =
+      List.fold_right
+        (fun e l ->
+           if List.mem e missing_method then l else CM_Virtual_method e::l)
+        (Concr.elements (Concr.diff sign2.cty_concr sign1.cty_concr))
+        error
+    in
+    match error with
+      [] ->
+        begin try
+          moregen_clty true type_pairs env patt subj;
+          []
+        with
+          Failure r -> r
+        end
+    | error ->
+        CM_Class_type_mismatch (patt, subj)::error
+  in
+  current_level := old_level;
+  res
+
+let rec equal_clty trace type_pairs subst env cty1 cty2 =
+  try
+    match cty1, cty2 with
+      Tcty_constr (_, _, cty1), Tcty_constr (_, _, cty2) ->
+        equal_clty true type_pairs subst env cty1 cty2
+    | Tcty_constr (_, _, cty1), _ ->
+        equal_clty true type_pairs subst env cty1 cty2
+    | _, Tcty_constr (_, _, cty2) ->
+        equal_clty true type_pairs subst env cty1 cty2
+    | Tcty_fun (ty1, cty1'), Tcty_fun (ty2, cty2') ->
+        begin try eqtype true type_pairs subst env ty1 ty2 with Unify trace ->
+          raise (Failure [CM_Parameter_mismatch (expand_trace env trace)])
+        end;
+        equal_clty false type_pairs subst env cty1' cty2'
+    | Tcty_signature sign1, Tcty_signature sign2 ->
+        let ty1 = object_fields (repr sign1.cty_self) in
+        let ty2 = object_fields (repr sign2.cty_self) in
+        let (fields1, rest1) = flatten_fields ty1
+        and (fields2, rest2) = flatten_fields ty2 in
+        let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
+        List.iter
+          (fun (lab, k1, t1, k2, t2) ->
+             begin try eqtype true type_pairs subst env t1 t2 with
+               Unify trace ->
+                 raise (Failure [CM_Meth_type_mismatch
+                                    (lab, expand_trace env trace)])
+             end)
+          pairs;
+        Vars.iter
+          (fun lab (mut, ty) ->
+             let (mut', ty') = Vars.find lab sign1.cty_vars in
+             try eqtype true type_pairs subst env ty ty' with Unify trace ->
+               raise (Failure [CM_Val_type_mismatch
+                                  (lab, expand_trace env trace)]))
+          sign2.cty_vars
+    | _ ->
+        raise (Failure [])
+  with
+    Failure error when trace ->
+      raise (Failure (CM_Class_type_mismatch (cty1, cty2)::error))
 
+(* XXX On pourrait autoriser l'instantiation du type des parametres... *)
+let match_class_declarations env patt_params patt_type subj_params subj_type =
+  let type_pairs = ref [] in
+  let subst = ref [] in
+  let sign1 = signature_of_class_type patt_type in
+  let sign2 = signature_of_class_type subj_type in
+  let t1 = repr sign1.cty_self in
+  let t2 = repr sign2.cty_self in
+  type_pairs := (t1, t2) :: !type_pairs;
+  let (fields1, rest1) = flatten_fields (object_fields t1)
+  and (fields2, rest2) = flatten_fields (object_fields t2) in
+  let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
+  let error =
+    List.fold_right
+      (fun (lab, k, _) err ->
+        let err =
+          let k = field_kind_repr k in
+          begin match k with
+            Fvar r -> err
+          | _      -> CM_Hide_public lab::err
+          end
+        in
+        if Concr.mem lab sign1.cty_concr then err
+        else CM_Hide_virtual lab::err)
+      miss1 []
+  in
+  let missing_method = List.map (fun (m, _, _) -> m) miss2 in
+  let error =
+    (List.map (fun m -> CM_Missing_method m) missing_method) @ error
+  in
+  (* Always succeeds *)
+  eqtype true type_pairs subst env rest1 rest2;
+  let error =
+    List.fold_right
+      (fun (lab, k1, t1, k2, t2) err ->
+        let k1 = field_kind_repr k1 in
+        let k2 = field_kind_repr k2 in
+        match k1, k2 with
+          (Fvar _, Fvar _)
+        | (Fpresent, Fpresent) -> err
+        | (Fvar _, Fpresent)   -> CM_Private_method lab::err
+        | (Fpresent, Fabsent)  -> CM_Public_method lab::err
+        | _                    -> assert false)
+      pairs error
+  in
+  let error =
+    Vars.fold
+      (fun lab (mut, ty) err ->
+         try
+           let (mut', ty') = Vars.find lab sign1.cty_vars in
+           if mut = Mutable && mut' <> Mutable then
+             CM_Non_mutable_value lab::err
+           else
+             err
+         with Not_found ->
+           CM_Missing_value lab::err)
+      sign2.cty_vars error
   in
-    eqtype_list tyl1 tyl2
+  let error =
+    List.fold_right
+      (fun e l ->
+        if List.mem e missing_method then l else CM_Virtual_method e::l)
+      (Concr.elements (Concr.diff sign2.cty_concr sign1.cty_concr))
+      error
+  in
+  match error with
+    [] ->
+      begin try
+        let lp = List.length patt_params in
+        let ls = List.length subj_params in
+        if lp  <> ls then
+          raise (Failure [CM_Parameter_arity_mismatch (lp, ls)]);
+        List.iter2 (fun p s ->
+          try eqtype true type_pairs subst env p s with Unify trace ->
+            raise (Failure [CM_Type_parameter_mismatch
+                               (expand_trace env trace)]))
+          patt_params subj_params;
+        equal_clty false type_pairs subst env patt_type subj_type;
+        []
+      with
+        Failure r -> r
+      end
+  | error ->
+(* XXX Trace plus precise : afficher les signatures (???) *)
+      error
 
 
                               (***************)
@@ -1196,17 +1789,17 @@ let rec build_subtype env t =
   | Tarrow(t1, t2) ->
       let (t1', c1) = (t1, false) in
       let (t2', c2) = build_subtype env t2 in
-      if c1 or c2 then (new_global_ty (Tarrow(t1', t2')), true)
+      if c1 or c2 then (newty (Tarrow(t1', t2')), true)
       else (t, false)
   | Ttuple tlist ->
       let (tlist', clist) =
         List.split (List.map (build_subtype env) tlist)
       in
       if List.exists (function c -> c) clist then
-        (new_global_ty (Ttuple tlist'), true)
+        (newty (Ttuple tlist'), true)
       else (t, false)
   | Tconstr(p, tl, abbrev) when generic_abbrev env p ->
-      let t' = expand_abbrev env p tl abbrev t.level in
+      let t' = expand_abbrev env t in
       let (t'', c) = build_subtype env t' in
       if c then (t'', true)
       else (t, false)
@@ -1218,7 +1811,7 @@ let rec build_subtype env t =
       (begin try
          List.assq t !subtypes
        with Not_found ->
-         let t' = new_global_var () in
+         let t' = newvar () in
          subtypes := (t, t')::!subtypes;
          let (t1', _) = build_subtype env t1 in
          t'.desc <- Tobject (t1', ref None);
@@ -1228,9 +1821,9 @@ let rec build_subtype env t =
   | Tfield(s, _, t1, t2) (* Always present *) ->
       let (t1', _) = build_subtype env t1 in
       let (t2', _) = build_subtype env t2 in
-      (new_global_ty (Tfield(s, Fpresent, t1', t2')), true)
+      (newty (Tfield(s, Fpresent, t1', t2')), true)
   | Tnil ->
-      let v = new_global_var () in
+      let v = newvar () in
       (v, true)
 
 let enlarge_type env ty =
@@ -1255,76 +1848,76 @@ let enlarge_type env ty =
     [generic_abbrev ...]).
 *)
 
-let subtypes = ref [];;
+let subtypes = ref []
 
 let subtype_error env trace =
   raise (Subtype (expand_trace env (List.rev trace), []))
 
-let rec subtype_rec env trace t1 t2 =
+let rec subtype_rec env trace t1 t2 cstrs =
   let t1 = repr t1 in
   let t2 = repr t2 in
   if t1 == t2 then [] else
   if List.exists (fun (t1', t2') -> t1 == t1' & t2 == t2') !subtypes then
       (* +++ Possibly slow *)
-    []
+    cstrs
   else begin
     subtypes := (t1, t2) :: !subtypes;
     match (t1.desc, t2.desc) with
       (Tvar, _) | (_, Tvar) ->
-        [(trace, t1, t2)]
+        (trace, t1, t2)::cstrs
     | (Tarrow(t1, u1), Tarrow(t2, u2)) ->
-        (subtype_rec env ((t2, t1)::trace) t2 t1) @
-        (subtype_rec env ((u1, u2)::trace) u1 u2)
+        let cstrs = subtype_rec env ((t2, t1)::trace) t2 t1 cstrs in
+        subtype_rec env ((u1, u2)::trace) u1 u2 cstrs
     | (Ttuple tl1, Ttuple tl2) ->
-        subtype_list env trace tl1 tl2
+        subtype_list env trace tl1 tl2 cstrs
     | (Tconstr(p1, tl1, abbrev1), Tconstr _) when generic_abbrev env p1 ->
-        subtype_rec env trace (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
+        subtype_rec env trace (expand_abbrev env t1) t2 cstrs
     | (Tconstr _, Tconstr(p2, tl2, abbrev2)) when generic_abbrev env p2 ->
-        subtype_rec env trace t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
+        subtype_rec env trace t1 (expand_abbrev env t2) cstrs
     | (Tconstr _, Tconstr _) ->
-        [(trace, t1, t2)]
+        (trace, t1, t2)::cstrs
     | (Tconstr(p1, tl1, abbrev1), _) when generic_abbrev env p1 ->
-        subtype_rec env trace (expand_abbrev env p1 tl1 abbrev1 t1.level) t2
+        subtype_rec env trace (expand_abbrev env t1) t2 cstrs
     | (_, Tconstr (p2, tl2, abbrev2)) when generic_abbrev env p2 ->
-        subtype_rec env trace t1 (expand_abbrev env p2 tl2 abbrev2 t2.level)
+        subtype_rec env trace t1 (expand_abbrev env t2) cstrs
     | (Tobject (f1, _), Tobject (f2, _))
               when opened_object f1 & opened_object f2 ->
         (* Same row variable implies same object. *)
-        [(trace, t1, t2)]
+        (trace, t1, t2)::cstrs
     | (Tobject (f1, _), Tobject (f2, _)) ->
-        subtype_fields env trace f1 f2
+        subtype_fields env trace f1 f2 cstrs
     | (_, _) ->
         subtype_error env trace
   end
 
-and subtype_list env trace tl1 tl2 =
+and subtype_list env trace tl1 tl2 cstrs =
   if List.length tl1 <> List.length tl2 then
     subtype_error env trace;
   List.fold_left2
-    (fun cstrs t1 t2 -> cstrs @ (subtype_rec env ((t1, t2)::trace) t1 t2))
-    [] tl1 tl2
+    (fun cstrs t1 t2 -> subtype_rec env ((t1, t2)::trace) t1 t2 cstrs)
+    cstrs tl1 tl2
 
-and subtype_fields env trace ty1 ty2 =
+and subtype_fields env trace ty1 ty2 cstrs =
   let (fields1, rest1) = flatten_fields ty1 in
   let (fields2, rest2) = flatten_fields ty2 in
   let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
-  [(trace, rest1, build_fields miss2 (newvar ()))]
+  [(trace, rest1, build_fields ty2.level miss2 (newvar ()))]
     @
   begin match rest2.desc with
     Tnil   -> []
-  | _      -> [(trace, build_fields miss1 rest1, rest2)]
+  | _      -> [(trace, build_fields ty1.level miss1 rest1, rest2)]
   end
     @
   (List.fold_left
-     (fun cstrs (k1, t1, k2, t2) ->
+     (fun cstrs (_, k1, t1, k2, t2) ->
         (* Theses fields are always present *)
-        cstrs @ (subtype_rec env ((t1, t2)::trace) t1 t2))
-     [] pairs)
+        subtype_rec env ((t1, t2)::trace) t1 t2 cstrs)
+     cstrs pairs)
 
 let subtype env ty1 ty2 =
   subtypes := [];
   (* Build constraint set. *)
-  let cstrs = subtype_rec env [(ty1, ty2)] ty1 ty2 in
+  let cstrs = subtype_rec env [(ty1, ty2)] ty1 ty2 [] in
   (* Enforce constraints. *)
   function () ->
     List.iter
@@ -1332,7 +1925,7 @@ let subtype env ty1 ty2 =
          try unify env t1 t2 with Unify trace ->
            raise (Subtype (expand_trace env (List.rev trace0),
                            List.tl (List.tl trace))))
-      cstrs;
+      (List.rev cstrs);
     subtypes := []
 
 
@@ -1419,7 +2012,7 @@ let rec nondep_type_rec env id ty =
           if Path.isfree id p then
             begin try
               Tlink (nondep_type_rec env id
-                       (expand_abbrev env p tl abbrev ty.level))
+                       (expand_abbrev env {desc = desc; level = ty.level}))
               (*
                  The [Tlink] is important. The expanded type may be a
                  variable, or may not be completely copied yet
@@ -1442,9 +2035,12 @@ let rec nondep_type_rec env id ty =
           begin match field_kind_repr kind with
             Fpresent ->
               Tfield(label, Fpresent, nondep_type_rec env id t1,
-                     nondep_type_rec env id t2)
-          | _ ->
-              Tlink (nondep_type_rec env id t2)
+                                      nondep_type_rec env id t2)
+          | Fvar _ (* {contents = None} *) as k ->
+              Tfield(label, k, nondep_type_rec env id t1,
+                               nondep_type_rec env id t2)
+          | Fabsent ->
+              assert false
           end
       | Tnil ->
           Tnil
@@ -1516,88 +2112,54 @@ let nondep_type_decl env mid id is_covariant decl =
     raise Not_found
 
 (* Preserve sharing inside class types. *)
-let nondep_class_type env id decl =
-  try
-    let decl =
-      { cty_params = List.map (nondep_type_rec env id) decl.cty_params;
-        cty_args = List.map (nondep_type_rec env id) decl.cty_args;
-        cty_vars =
-          Vars.map (function (m, t) -> (m, nondep_type_rec env id t))
-            decl.cty_vars;
-        cty_meths = Meths.map (nondep_type_rec env id) decl.cty_meths;
-        cty_self = nondep_type_rec env id decl.cty_self;
-        cty_concr = decl.cty_concr;
-        cty_new =
-          begin match decl.cty_new with
-            None    -> None
-          | Some ty -> Some (nondep_type_rec env id ty)
-          end }
-    in
-    cleanup_types ();
-    List.iter unmark_type decl.cty_params;
-    List.iter unmark_type decl.cty_args;
-    Vars.iter (fun l (m, t) -> unmark_type t) decl.cty_vars;
-    Meths.iter (fun l t -> unmark_type t) decl.cty_meths;
-    unmark_type decl.cty_self;
-    begin match decl.cty_new with
-      None    -> ()
-    | Some ty -> unmark_type ty
-    end;
-    decl
-  with Not_found ->
-    cleanup_types ();
-    raise Not_found
-
-
-                    (**************************************)
-                    (*  Check genericity of type schemes  *)
-                    (**************************************)
-
-
-type closed_schema_result = Var of type_expr | Row_var of type_expr
-exception Failed of closed_schema_result
-
-let rec closed_schema_rec row ty =
-  let ty = repr ty in
-  if ty.level >= lowest_level then begin
-    let level = ty.level in
-    ty.level <- pivot_level - level;
-    match ty.desc with
-      Tvar when level <> generic_level ->
-        raise (Failed (if row then Row_var ty else Var ty))
-    | Tobject(f, {contents = Some (_, p)}) ->
-        closed_schema_rec true f;
-        List.iter (closed_schema_rec false) p
-    | Tobject(f, _) ->
-        closed_schema_rec true f
-    | Tfield(_, kind, t1, t2) ->
-        if field_kind_repr kind = Fpresent then
-          closed_schema_rec false t1;
-        closed_schema_rec true t2
-    | _ ->
-        iter_type_expr (closed_schema_rec false) ty
-  end
-
-(* Return whether all variables of type [ty] are generic. *)
-let closed_schema ty =
-  try
-    closed_schema_rec false ty;
-    unmark_type ty;
-    true
-  with Failed _ ->
-    unmark_type ty;
-    false
-
-(*
-    Check that all variables of type [ty] are generic. If this is not
-    the case, the non-generic variable is returned. The type is never
-    generalized.
-*)
-let closed_schema_verbose ty =
-  try
-    closed_schema_rec false ty;
-    unmark_type ty;
-    None
-  with Failed status ->
-    unmark_type ty;
-    Some status
+let nondep_class_signature env id sign =
+  { cty_self = nondep_type_rec env id sign.cty_self;
+    cty_vars =
+      Vars.map (function (m, t) -> (m, nondep_type_rec env id t))
+        sign.cty_vars;
+    cty_concr = sign.cty_concr }
+
+let rec nondep_class_type env id =
+  function
+    Tcty_constr (p, _, cty) when Path.isfree id p ->
+      nondep_class_type env id cty
+  | Tcty_constr (p, tyl, cty) ->
+      Tcty_constr (p, List.map (nondep_type_rec env id) tyl,
+                   nondep_class_type env id cty)
+  | Tcty_signature sign ->
+      Tcty_signature (nondep_class_signature env id sign)
+  | Tcty_fun (ty, cty) ->
+      Tcty_fun (nondep_type_rec env id ty, nondep_class_type env id cty)
+
+let nondep_class_declaration env id decl =
+  assert (not (Path.isfree id decl.cty_path));
+  let decl =
+    { cty_params = List.map (nondep_type_rec env id) decl.cty_params;
+      cty_type = nondep_class_type env id decl.cty_type;
+      cty_path = decl.cty_path;
+      cty_new =
+        begin match decl.cty_new with
+          None    -> None
+        | Some ty -> Some (nondep_type_rec env id ty)
+        end }
+  in
+  cleanup_types ();
+  List.iter unmark_type decl.cty_params;
+  unmark_class_type decl.cty_type;
+  begin match decl.cty_new with
+    None    -> ()
+  | Some ty -> unmark_type ty
+  end;
+  decl
+
+let nondep_cltype_declaration env id decl =
+  assert (not (Path.isfree id decl.clty_path));
+  let decl =
+    { clty_params = List.map (nondep_type_rec env id) decl.clty_params;
+      clty_type = nondep_class_type env id decl.clty_type;
+      clty_path = decl.clty_path }
+  in
+  cleanup_types ();
+  List.iter unmark_type decl.clty_params;
+  unmark_class_type decl.clty_type;
+  decl
diff --git a/typing/ctype.mli b/typing/ctype.mli
index c5b2f9c421..a88cd01e2e 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -29,7 +29,11 @@ val begin_def: unit -> unit
         (* Raise the variable level by one at the beginning of a definition. *)
 val end_def: unit -> unit
         (* Lower the variable level by one at the end of a definition *)
+val begin_class_def: unit -> unit
+val raise_nongen_level: unit -> unit
 val reset_global_level: unit -> unit
+val increase_global_level: unit -> unit
+val restore_global_level: unit -> unit
 
 val newty: type_desc -> type_expr
 val newgenty: type_desc -> type_expr
@@ -39,28 +43,44 @@ val new_global_var: unit -> type_expr
         (* Return a fresh variable, bound at toplevel
            (as type variables ['a] in type constraints). *)
 val newobj: type_expr -> type_expr
+val newconstr: Path.t -> type_expr list -> type_expr
 val none: type_expr
         (* A dummy type expression *)
 
 val repr: type_expr -> type_expr
         (* Return the canonical representative of a type. *)
 
-val flatten_fields :
+val object_fields: type_expr -> type_expr
+val flatten_fields:
         type_expr -> (string * field_kind * type_expr) list * type_expr
         (* Transform a field type into a list of pairs label-type *)
+        (* The fields are sorted *)
+val associate_fields:
+        (string * field_kind * type_expr) list ->
+        (string * field_kind * type_expr) list ->
+        (string * field_kind * type_expr * field_kind * type_expr) list *
+        (string * field_kind * type_expr) list *
+        (string * field_kind * type_expr) list
 val opened_object: type_expr -> bool
 val close_object: type_expr -> unit
+val row_variable: type_expr -> type_expr
+        (* Return the row variable of an open object type *)
 val set_object_name:
-        type_expr -> type_expr list -> Ident.t -> unit
+        Ident.t -> type_expr -> type_expr list -> type_expr -> unit
 val remove_object_name: type_expr -> unit
 val hide_private_methods: type_expr -> unit
 
 val generalize: type_expr -> unit
         (* Generalize in-place the given type *)
+val iterative_generalization: int -> type_expr list -> type_expr list
+        (* Efficient repeated generalization of a type *)
 val make_nongen: type_expr -> unit
         (* Make non-generalizable the given type *)
 val correct_levels: type_expr -> type_expr
         (* Returns a copy with decreasing levels *)
+val limited_generalize: type_expr -> type_expr -> unit
+        (* Only generalize some part of the type
+           Make the remaining of the type non-generalizable *)
 
 val instance: type_expr -> type_expr
         (* Take an instance of a type scheme *)
@@ -77,19 +97,13 @@ val instance_parameterized_type_2:
         type_expr list -> type_expr list -> type_expr ->
         type_expr list * type_expr list * type_expr
 val instance_class:
-        class_type ->
-        type_expr list * type_expr list * (mutable_flag * type_expr) Vars.t *
-        type_expr Meths.t * type_expr
+        type_expr list -> class_type -> type_expr list * class_type
 val apply:
         Env.t -> type_expr list -> type_expr -> type_expr list -> type_expr
         (* [apply [p1...pN] t [a1...aN]] match the arguments [ai] to
         the parameters [pi] and returns the corresponding instance of
         [t]. Exception [Cannot_apply] is raised in case of failure. *)
 
-(* val expand_abbrev: *)
-(*         Env.t -> Path.t -> type_expr list -> Types.abbrev_memo ref -> *)
-(*         int -> type_expr *)
-(*         (* Expand an abbreviation *) *)
 val expand_head: Env.t -> type_expr -> type_expr
 val full_expand: Env.t -> type_expr -> type_expr
 
@@ -99,14 +113,38 @@ val filter_arrow: Env.t -> type_expr -> type_expr * type_expr
         (* A special case of unification (with 'a -> 'b). *)
 val filter_method: Env.t -> string -> private_flag -> type_expr -> type_expr
         (* A special case of unification (with {m : 'a; 'b}). *)
-
+val filter_self_method:
+        Env.t -> string -> private_flag -> (Ident.t * type_expr) Meths.t ref ->
+        type_expr -> Ident.t * type_expr
 val moregeneral: Env.t -> bool -> type_expr -> type_expr -> bool
         (* Check if the first type scheme is more general than the second. *)
-
+type class_match_failure =
+    CM_Virtual_class
+  | CM_Parameter_arity_mismatch of int * int
+  | CM_Type_parameter_mismatch of (type_expr * type_expr) list
+  | CM_Class_type_mismatch of class_type * class_type
+  | CM_Parameter_mismatch of (type_expr * type_expr) list
+  | CM_Val_type_mismatch of string * (type_expr * type_expr) list
+  | CM_Meth_type_mismatch of string * (type_expr * type_expr) list
+  | CM_Non_mutable_value of string
+  | CM_Missing_value of string
+  | CM_Missing_method of string
+  | CM_Hide_public of string
+  | CM_Hide_virtual of string
+  | CM_Public_method of string
+  | CM_Private_method of string
+  | CM_Virtual_method of string
+val match_class_types:
+        Env.t -> class_type -> class_type -> class_match_failure list
+        (* Check if the first class type is more general than the second. *)
 val equal: Env.t -> bool -> type_expr list -> type_expr list -> bool
         (* [equal env [x1...xn] tau [y1...yn] sigma]
            checks whether the parameterized types
            [/\x1.../\xn.tau] and [/\y1.../\yn.sigma] are equivalent. *)
+val match_class_declarations:
+        Env.t -> type_expr list -> class_type -> type_expr list ->
+        class_type -> class_match_failure list
+        (* Check if the first class type is more general than the second. *)
 
 val enlarge_type: Env.t -> type_expr -> type_expr
         (* Make a type larger *)
@@ -124,19 +162,30 @@ val nondep_type_decl:
         Env.t -> Ident.t -> Ident.t -> bool -> type_declaration ->
         type_declaration
         (* Same for type declarations. *)
-val nondep_class_type: Env.t -> Ident.t -> class_type -> class_type
-        (* Same for class types. *)
-
+val nondep_class_declaration:
+        Env.t -> Ident.t -> class_declaration -> class_declaration
+        (* Same for class declarations. *)
+val nondep_cltype_declaration:
+        Env.t -> Ident.t -> cltype_declaration -> cltype_declaration
+        (* Same for class type declarations. *)
 val correct_abbrev: Env.t -> Ident.t -> type_expr list -> type_expr -> unit
 val cyclic_abbrev: Env.t -> Ident.t -> type_expr -> bool
 
-type closed_schema_result = Var of type_expr | Row_var of type_expr
 val closed_schema: type_expr -> bool
-val closed_schema_verbose: type_expr -> closed_schema_result option
         (* Check whether the given type scheme contains no non-generic
            type variables *)
 
+val closed_type_decl: type_declaration -> type_expr option
+type closed_class_failure =
+    CC_Method of type_expr * string * type_expr
+  | CC_Value of type_expr * string * type_expr
+val closed_class:
+        type_expr list -> class_signature -> closed_class_failure option
+        (* Check whether all type variables are bound *)
+
 val unalias: type_expr -> type_expr
-val unroll_abbrev: Ident.t -> type_expr list -> type_expr -> type_expr
+val signature_of_class_type: class_type -> class_signature
+val self_type: class_type -> type_expr
+val class_type_arity: class_type -> int
 val arity: type_expr -> int
         (* Return the arity (as for curried functions) of the given type. *)
diff --git a/typing/env.ml b/typing/env.ml
index 0e12be9261..23b848731b 100644
--- a/typing/env.ml
+++ b/typing/env.ml
@@ -37,7 +37,8 @@ type summary =
   | Env_exception of summary * Ident.t * exception_declaration
   | Env_module of summary * Ident.t * module_type
   | Env_modtype of summary * Ident.t * modtype_declaration
-  | Env_class of summary * Ident.t * class_type
+  | Env_class of summary * Ident.t * class_declaration
+  | Env_cltype of summary * Ident.t * cltype_declaration
   | Env_open of summary * Path.t
 
 type t = {
@@ -48,7 +49,8 @@ type t = {
   modules: (Path.t * module_type) Ident.tbl;
   modtypes: (Path.t * modtype_declaration) Ident.tbl;
   components: (Path.t * module_components) Ident.tbl;
-  classes: (Path.t * class_type) Ident.tbl;
+  classes: (Path.t * class_declaration) Ident.tbl;
+  cltypes: (Path.t * cltype_declaration) Ident.tbl;
   summary: summary
 }
 
@@ -64,7 +66,8 @@ and structure_components = {
   mutable comp_modules: (string, (module_type * int)) Tbl.t;
   mutable comp_modtypes: (string, (modtype_declaration * int)) Tbl.t;
   mutable comp_components: (string, (module_components * int)) Tbl.t;
-  mutable comp_classes: (string, (class_type * int)) Tbl.t
+  mutable comp_classes: (string, (class_declaration * int)) Tbl.t;
+  mutable comp_cltypes: (string, (cltype_declaration * int)) Tbl.t
 }
 
 and functor_components = {
@@ -79,6 +82,7 @@ let empty = {
   labels = Ident.empty; types = Ident.empty;
   modules = Ident.empty; modtypes = Ident.empty;
   components = Ident.empty; classes = Ident.empty;
+  cltypes = Ident.empty;
   summary = Env_empty }
 
 (* Persistent structure descriptions *)
@@ -189,6 +193,8 @@ and find_modtype =
   find (fun env -> env.modtypes) (fun sc -> sc.comp_modtypes)
 and find_class =
   find (fun env -> env.classes) (fun sc -> sc.comp_classes)
+and find_cltype =
+  find (fun env -> env.cltypes) (fun sc -> sc.comp_cltypes)
 
 let find_type_expansion path env =
   let decl = find_type path env in
@@ -327,6 +333,8 @@ and lookup_modtype =
   lookup (fun env -> env.modtypes) (fun sc -> sc.comp_modtypes)
 and lookup_class =
   lookup (fun env -> env.classes) (fun sc -> sc.comp_classes)
+and lookup_cltype =
+  lookup (fun env -> env.cltypes) (fun sc -> sc.comp_cltypes)
   
 (* Scrape a module type *)
 
@@ -392,11 +400,14 @@ let rec prefix_idents root pos sub = function
       (p::pl, final_sub)
   | Tsig_class(id, decl) :: rem ->
       let p = Pdot(root, Ident.name id, pos) in
-      let (pl, final_sub) =
-        prefix_idents root (pos + 1) sub rem
-      in
+      let (pl, final_sub) = prefix_idents root (pos + 1) sub rem in
+      (p::pl, final_sub)
+  | Tsig_cltype(id, decl) :: rem ->
+      let p = Pdot(root, Ident.name id, nopos) in
+      let (pl, final_sub) = prefix_idents root pos sub rem in
       (p::pl, final_sub)
 
+
 (* Compute structure descriptions *)
 
 let rec components_of_module env sub path mty =
@@ -406,7 +417,8 @@ let rec components_of_module env sub path mty =
         { comp_values = Tbl.empty; comp_constrs = Tbl.empty;
           comp_labels = Tbl.empty; comp_types = Tbl.empty;
           comp_modules = Tbl.empty; comp_modtypes = Tbl.empty;
-          comp_components = Tbl.empty; comp_classes = Tbl.empty } in
+          comp_components = Tbl.empty; comp_classes = Tbl.empty;
+          comp_cltypes = Tbl.empty } in
       let (pl, sub) = prefix_idents path 0 sub sg in
       let env = ref env in
       let pos = ref 0 in
@@ -452,10 +464,14 @@ let rec components_of_module env sub path mty =
               Tbl.add (Ident.name id) (decl', nopos) c.comp_modtypes;
             env := store_modtype id path decl' !env
         | Tsig_class(id, decl) ->
-            let decl' = Subst.class_type sub decl in
+            let decl' = Subst.class_declaration sub decl in
             c.comp_classes <-
               Tbl.add (Ident.name id) (decl', !pos) c.comp_classes;
-            incr pos)
+            incr pos
+        | Tsig_cltype(id, decl) ->
+            let decl' = Subst.cltype_declaration sub decl in
+            c.comp_cltypes <-
+              Tbl.add (Ident.name id) (decl', !pos) c.comp_cltypes)
         sg pl;
         Structure_comps c
   | Tmty_functor(param, ty_arg, ty_res) ->
@@ -469,7 +485,8 @@ let rec components_of_module env sub path mty =
           comp_values = Tbl.empty; comp_constrs = Tbl.empty;
           comp_labels = Tbl.empty; comp_types = Tbl.empty;
           comp_modules = Tbl.empty; comp_modtypes = Tbl.empty;
-          comp_components = Tbl.empty; comp_classes = Tbl.empty }
+          comp_components = Tbl.empty; comp_classes = Tbl.empty;
+          comp_cltypes = Tbl.empty }
 
 (* Insertion of bindings by identifier + path *)
 
@@ -482,6 +499,7 @@ and store_value id path decl env =
     modtypes = env.modtypes;
     components = env.components;
     classes = env.classes;
+    cltypes = env.cltypes;
     summary = Env_value(env.summary, id, decl) }
 
 and store_type id path info env =
@@ -503,6 +521,7 @@ and store_type id path info env =
     modtypes = env.modtypes;
     components = env.components;
     classes = env.classes;
+    cltypes = env.cltypes;
     summary = Env_type(env.summary, id, info) }
 
 and store_exception id path decl env =
@@ -514,6 +533,7 @@ and store_exception id path decl env =
     modtypes = env.modtypes;
     components = env.components;
     classes = env.classes;
+    cltypes = env.cltypes;
     summary = Env_exception(env.summary, id, decl) }
 
 and store_module id path mty env =
@@ -527,6 +547,7 @@ and store_module id path mty env =
       Ident.add id (path, components_of_module env Subst.identity path mty)
                    env.components;
     classes = env.classes;
+    cltypes = env.cltypes;
     summary = Env_module(env.summary, id, mty) }
 
 and store_modtype id path info env =
@@ -538,6 +559,7 @@ and store_modtype id path info env =
     modtypes = Ident.add id (path, info) env.modtypes;
     components = env.components;
     classes = env.classes;
+    cltypes = env.cltypes;
     summary = Env_modtype(env.summary, id, info) }
 
 and store_components id path comps env =
@@ -549,6 +571,7 @@ and store_components id path comps env =
     modtypes = env.modtypes;
     components = Ident.add id (path, comps) env.components;
     classes = env.classes;
+    cltypes = env.cltypes;
     summary = env.summary }
 
 and store_class id path desc env =
@@ -560,8 +583,21 @@ and store_class id path desc env =
     modtypes = env.modtypes;
     components = env.components;
     classes = Ident.add id (path, desc) env.classes;
+    cltypes = env.cltypes;
     summary = Env_class(env.summary, id, desc) }
 
+and store_cltype id path desc env =
+  { values = env.values;
+    constrs = env.constrs;
+    labels = env.labels;
+    types = env.types;
+    modules = env.modules;
+    modtypes = env.modtypes;
+    components = env.components;
+    classes = env.classes;
+    cltypes = Ident.add id (path, desc) env.cltypes;
+    summary = Env_cltype(env.summary, id, desc) }
+
 (* Memoized function to compute the components of a functor application
    in a path. *)
 
@@ -602,6 +638,9 @@ and add_modtype id info env =
 and add_class id ty env =
   store_class id (Pident id) ty env
 
+and add_cltype id ty env =
+  store_cltype id (Pident id) ty env
+
 (* Insertion of bindings by name *)
 
 let enter store_fun name data env =
@@ -613,17 +652,19 @@ and enter_exception = enter store_exception
 and enter_module = enter store_module
 and enter_modtype = enter store_modtype
 and enter_class = enter store_class
+and enter_cltype = enter store_cltype
 
 (* Insertion of all components of a signature *)
 
 let add_item comp env =
   match comp with
-    Tsig_value(id, decl) -> add_value id decl env
-  | Tsig_type(id, decl) -> add_type id decl env
+    Tsig_value(id, decl)     -> add_value id decl env
+  | Tsig_type(id, decl)      -> add_type id decl env
   | Tsig_exception(id, decl) -> add_exception id decl env
-  | Tsig_module(id, mty) -> add_module id mty env
-  | Tsig_modtype(id, decl) -> add_modtype id decl env
-  | Tsig_class(id, decl) -> add_class id decl env
+  | Tsig_module(id, mty)     -> add_module id mty env
+  | Tsig_modtype(id, decl)   -> add_modtype id decl env
+  | Tsig_class(id, decl)     -> add_class id decl env
+  | Tsig_cltype(id, decl)    -> add_cltype id decl env
 
 let rec add_signature sg env =
   match sg with
@@ -656,7 +697,10 @@ let open_signature root sg env =
                           (Subst.modtype_declaration sub decl) env
         | Tsig_class(id, decl) ->
             store_class (Ident.hide id) p
-                        (Subst.class_type sub decl) env)
+                        (Subst.class_declaration sub decl) env
+        | Tsig_cltype(id, decl) ->
+            store_cltype (Ident.hide id) p
+                         (Subst.cltype_declaration sub decl) env)
       env sg pl in
   { values = newenv.values;
     constrs = newenv.constrs;
@@ -666,6 +710,7 @@ let open_signature root sg env =
     modtypes = newenv.modtypes;
     components = newenv.components;
     classes = newenv.classes;
+    cltypes = newenv.cltypes;
     summary = Env_open(env.summary, root) }
   
 (* Open a signature from a file *)
diff --git a/typing/env.mli b/typing/env.mli
index d3d0ee7f78..4a19f144a2 100644
--- a/typing/env.mli
+++ b/typing/env.mli
@@ -26,7 +26,8 @@ val find_value: Path.t -> t -> value_description
 val find_type: Path.t -> t -> type_declaration
 val find_module: Path.t -> t -> module_type
 val find_modtype: Path.t -> t -> modtype_declaration
-val find_class: Path.t -> t -> class_type
+val find_class: Path.t -> t -> class_declaration
+val find_cltype: Path.t -> t -> cltype_declaration
 
 val find_type_expansion: Path.t -> t -> type_expr list * type_expr
 val find_modtype_expansion: Path.t -> t -> Types.module_type
@@ -39,7 +40,8 @@ val lookup_label: Longident.t -> t -> label_description
 val lookup_type: Longident.t -> t -> Path.t * type_declaration
 val lookup_module: Longident.t -> t -> Path.t * module_type
 val lookup_modtype: Longident.t -> t -> Path.t * modtype_declaration
-val lookup_class: Longident.t -> t -> Path.t * class_type
+val lookup_class: Longident.t -> t -> Path.t * class_declaration
+val lookup_cltype: Longident.t -> t -> Path.t * cltype_declaration
 
 (* Insertion by identifier *)
 
@@ -48,7 +50,8 @@ val add_type: Ident.t -> type_declaration -> t -> t
 val add_exception: Ident.t -> exception_declaration -> t -> t
 val add_module: Ident.t -> module_type -> t -> t
 val add_modtype: Ident.t -> modtype_declaration -> t -> t
-val add_class: Ident.t -> class_type -> t -> t
+val add_class: Ident.t -> class_declaration -> t -> t
+val add_cltype: Ident.t -> cltype_declaration -> t -> t
 
 (* Insertion of all fields of a signature. *)
 
@@ -68,7 +71,8 @@ val enter_type: string -> type_declaration -> t -> Ident.t * t
 val enter_exception: string -> exception_declaration -> t -> Ident.t * t
 val enter_module: string -> module_type -> t -> Ident.t * t
 val enter_modtype: string -> modtype_declaration -> t -> Ident.t * t
-val enter_class: string -> class_type -> t -> Ident.t * t
+val enter_class: string -> class_declaration -> t -> Ident.t * t
+val enter_cltype: string -> cltype_declaration -> t -> Ident.t * t
 
 (* Reset the cache of in-core module interfaces.
    To be called in particular when load_path changes. *)
@@ -96,7 +100,8 @@ type summary =
   | Env_exception of summary * Ident.t * exception_declaration
   | Env_module of summary * Ident.t * module_type
   | Env_modtype of summary * Ident.t * modtype_declaration
-  | Env_class of summary * Ident.t * class_type
+  | Env_class of summary * Ident.t * class_declaration
+  | Env_cltype of summary * Ident.t * cltype_declaration
   | Env_open of summary * Path.t
 
 val summary: t -> summary
diff --git a/typing/includecore.ml b/typing/includecore.ml
index e3f7b75cf7..8eb7c0e338 100644
--- a/typing/includecore.ml
+++ b/typing/includecore.ml
@@ -107,32 +107,3 @@ let vars vars1 vars2 =
         end,
         encode_val v2 vl2))
     vars2 ([], [])
-
-let class_types env d1 d2 =
-  (* Same abbreviations *)
-  Ctype.equal env true
-    (d1.cty_self::d1.cty_params) (d2.cty_self::d2.cty_params)
-      &&
-  (* Fewer concretes methods *)
-  Concr.subset d2.cty_concr d1.cty_concr
-      &&
-  (* If virtual, stays virtual *)
-  (d1.cty_new <> None or d2.cty_new = None)
-      &&
-  (* Virtual methods cannot be hidden *)
-  Meths.fold
-    (fun lab ty res ->
-       res &&
-       (Concr.mem lab d1.cty_concr ||
-        try Meths.find lab d2.cty_meths; true with Not_found -> false))
-    d1.cty_meths
-    true
-      &&
-  (* Less general *)
-  let (m1, m2) = meths d1.cty_meths d2.cty_meths in
-  let (v1, v2) = vars d1.cty_vars d2.cty_vars in
-  let t1 = Ctype.newgenty (Ttuple (d1.cty_self::m1@v1@d1.cty_args)) in
-  let t2 = Ctype.newgenty (Ttuple (d2.cty_self::m2@v2@d2.cty_args)) in
-  List.length d1.cty_args = List.length d2.cty_args
-      &&
-  Ctype.moregeneral env true t1 t2
diff --git a/typing/includecore.mli b/typing/includecore.mli
index 11fe4e4a29..1e87b023b9 100644
--- a/typing/includecore.mli
+++ b/typing/includecore.mli
@@ -24,5 +24,7 @@ val type_declarations:
         Env.t -> Ident.t -> type_declaration -> type_declaration -> bool
 val exception_declarations:
         Env.t -> exception_declaration -> exception_declaration -> bool
+(*
 val class_types:
         Env.t -> class_type -> class_type -> bool
+*)
diff --git a/typing/includemod.ml b/typing/includemod.ml
index 0a962142b1..098b820255 100644
--- a/typing/includemod.ml
+++ b/typing/includemod.ml
@@ -28,7 +28,12 @@ type error =
   | Modtype_infos of Ident.t * modtype_declaration * modtype_declaration
   | Modtype_permutation
   | Interface_mismatch of string * string
-  | Class_types of Ident.t * class_type * class_type
+  | Class_type_declarations of
+      Ident.t * cltype_declaration * cltype_declaration *
+      Ctype.class_match_failure list
+  | Class_declarations of
+      Ident.t * class_declaration * class_declaration *
+      Ctype.class_match_failure list
 
 exception Error of error list
 
@@ -61,13 +66,19 @@ let exception_declarations env subst id decl1 decl2 =
   then ()
   else raise(Error[Exception_declarations(id, decl1, decl2)])
 
-(* Inclusion between class types *)
+(* Inclusion between class declarations *)
 
-let class_types env subst id decl1 decl2 =
-  let decl2 = Subst.class_type subst decl2 in
-  if Includecore.class_types env decl1 decl2
-  then ()
-  else raise(Error[Class_types(id, decl1, decl2)])
+let class_type_declarations env subst id decl1 decl2 =
+  let decl2 = Subst.cltype_declaration subst decl2 in
+  match Includeclass.class_type_declarations env decl1 decl2 with
+    []     -> ()
+  | reason -> raise(Error[Class_type_declarations(id, decl1, decl2, reason)])
+
+let class_declarations env subst id decl1 decl2 =
+  let decl2 = Subst.class_declaration subst decl2 in
+  match Includeclass.class_declarations env decl1 decl2 with
+    []     -> ()
+  | reason -> raise(Error[Class_declarations(id, decl1, decl2, reason)])
 
 (* Expand a module type identifier when possible *)
 
@@ -87,6 +98,7 @@ type field_desc =
   | Field_exception of string
   | Field_module of string
   | Field_modtype of string
+  | Field_class of string
   | Field_classtype of string
 
 let item_ident_name = function
@@ -95,7 +107,8 @@ let item_ident_name = function
   | Tsig_exception(id, _) -> (id, Field_exception(Ident.name id))
   | Tsig_module(id, _) -> (id, Field_module(Ident.name id))
   | Tsig_modtype(id, _) -> (id, Field_modtype(Ident.name id))
-  | Tsig_class(id, _) -> (id, Field_classtype(Ident.name id))
+  | Tsig_class(id, _) -> (id, Field_class(Ident.name id))
+  | Tsig_cltype(id, _) -> (id, Field_classtype(Ident.name id))
 
 (* Simplify a structure coercion *)
 
@@ -155,7 +168,7 @@ and try_modtypes2 env mty1 mty2 =
   | (_, Tmty_ident p2) ->
       try_modtypes env Subst.identity mty1 (expand_module_path env p2)
   | (_, _) ->
-      fatal_error "Includemod.try_modtypes2"
+      assert false
 
 (* Inclusion between signatures *)
 
@@ -173,7 +186,8 @@ and signatures env subst sig1 sig2 =
           match item with
             Tsig_value(_,{val_kind = Val_prim _})
           | Tsig_type(_,_)
-          | Tsig_modtype(_,_) -> pos
+          | Tsig_modtype(_,_)
+          | Tsig_cltype(_,_) -> pos
           | Tsig_value(_,_)
           | Tsig_exception(_,_)
           | Tsig_module(_,_)
@@ -205,7 +219,7 @@ and signatures env subst sig1 sig2 =
                 Subst.add_module id2 (Pident id1) subst
             | Tsig_modtype _ ->
                 Subst.add_modtype id2 (Tmty_ident (Pident id1)) subst
-            | Tsig_value _ | Tsig_exception _ | Tsig_class _ ->
+            | Tsig_value _ | Tsig_exception _ | Tsig_class _ | Tsig_cltype _ ->
                 subst
           in
           pair_components new_subst
@@ -240,10 +254,13 @@ and signature_components env subst = function
       modtype_infos env subst id1 info1 info2;
       signature_components env subst rem
   | (Tsig_class(id1, decl1), Tsig_class(id2, decl2), pos) :: rem ->
-      class_types env subst id1 decl1 decl2;
+      class_declarations env subst id1 decl1 decl2;
       (pos, Tcoerce_none) :: signature_components env subst rem
+  | (Tsig_cltype(id1, info1), Tsig_cltype(id2, info2), pos) :: rem ->
+      class_type_declarations env subst id1 info1 info2;
+      signature_components env subst rem
   | _ ->
-      fatal_error "Includemod.signature_components"
+      assert false
 
 (* Inclusion between module type specifications *)
 
@@ -352,14 +369,26 @@ let include_err = function
       print_string intf_name;
       print_string ":";
       close_box()
-  | Class_types(id, d1, d2) ->
+  | Class_type_declarations(id, d1, d2, reason) ->
       open_hvbox 2;
-      print_string "Class types do not match:"; print_space();
-      Printtyp.class_type id d1; 
+      print_string "Class type declarations do not match:"; print_space();
+      Printtyp.cltype_declaration id d1; 
       print_break 1 (-2);
       print_string "is not included in"; print_space();
-      Printtyp.class_type id d2;
-      close_box()
+      Printtyp.cltype_declaration id d2;
+      close_box(),
+      print_space ();
+      Includeclass.report_error reason
+  | Class_declarations(id, d1, d2, reason) ->
+      open_hvbox 2;
+      print_string "Class declarations do not match:"; print_space();
+      Printtyp.class_declaration id d1; 
+      print_break 1 (-2);
+      print_string "is not included in"; print_space();
+      Printtyp.class_declaration id d2;
+      close_box();
+      print_space ();
+      Includeclass.report_error reason
 
 let report_error errlist =
   match errlist with
diff --git a/typing/includemod.mli b/typing/includemod.mli
index 65761d1b0f..2b80fc0f7c 100644
--- a/typing/includemod.mli
+++ b/typing/includemod.mli
@@ -32,7 +32,12 @@ type error =
   | Modtype_infos of Ident.t * modtype_declaration * modtype_declaration
   | Modtype_permutation
   | Interface_mismatch of string * string
-  | Class_types of Ident.t * class_type * class_type
+  | Class_type_declarations of
+      Ident.t * cltype_declaration * cltype_declaration *
+      Ctype.class_match_failure list
+  | Class_declarations of
+      Ident.t * class_declaration * class_declaration *
+      Ctype.class_match_failure list
 
 exception Error of error list
 
diff --git a/typing/mtype.ml b/typing/mtype.ml
index 09d71f0624..b9d0051a8f 100644
--- a/typing/mtype.ml
+++ b/typing/mtype.ml
@@ -72,6 +72,8 @@ and strengthen_sig env sg p =
       (* Need to add the module type in case it is manifest *)
   | (Tsig_class(id, decl) as sigelt) :: rem ->
       sigelt :: strengthen_sig env rem p
+  | (Tsig_cltype(id, decl) as sigelt) :: rem ->
+      sigelt :: strengthen_sig env rem p
 
 (* In nondep_supertype, env is only used for the type it assigns to id.
    Hence there is no need to keep env up-to-date by adding the bindings
@@ -117,7 +119,9 @@ let nondep_supertype env mid mty =
             | _  -> raise Not_found
           end
       | Tsig_class(id, d) ->
-          Tsig_class(id, Ctype.nondep_class_type env mid d) :: rem'
+          Tsig_class(id, Ctype.nondep_class_declaration env mid d) :: rem'
+      | Tsig_cltype(id, d) ->
+          Tsig_cltype(id, Ctype.nondep_cltype_declaration env mid d) :: rem'
 
   and nondep_modtype_decl = function
       Tmodtype_abstract -> Tmodtype_abstract
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index 57d2f0991b..c654b86c45 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -207,7 +207,7 @@ let rec typexp sch prio0 ty =
       if prio0 >= 1 then print_string ")";
       close_box()
     end
-(* ; print_string "["; print_int ty.level; print_string "]" *)
+(*; print_string "["; print_int ty.level; print_string "]"*)
 
 and typlist sch prio sep = function
     [] -> ()
@@ -232,7 +232,8 @@ and typobject sch ty fi nm =
                   l)
            fields []
        in
-       typfields sch rest present_fields);
+       typfields sch rest
+         (Sort.list (fun (n, _) (n', _) -> n <= n') present_fields));
       print_string " >";
       close_box ()
   | Some (p, {desc = Tvar}::tyl) ->
@@ -401,13 +402,7 @@ let value_description id decl =
 
 (* Print a class type *)
 
-let class_arg arg =
-  print_space ();
-  open_box 1; print_string "(";
-  type_sch arg;
-  print_string ")"; close_box ()
-
-let class_var l (m, t) =
+let class_var sch l (m, t) =
   print_space ();
   open_box 2;
   print_string "val ";
@@ -418,78 +413,202 @@ let class_var l (m, t) =
   print_string l;
   print_string " :";
   print_space();
-  type_sch t;
+  typexp sch 0 t;
   close_box()
 
-let metho public concrete lab ty =
-  print_space ();
-  open_box 2;
-  if Concr.mem lab concrete then print_string "method "
-  else print_string "virtual ";
-  if not (List.mem_assoc lab public) then print_string "protected ";
-  print_string lab;
-  print_string " :";
-  print_space ();
-  type_sch ty;
-  close_box ()
+let metho sch concrete (lab, kind, ty) =
+  if lab <> "*dummy method*" then begin
+    print_space ();
+    open_box 2;
+    print_string "method ";
+    begin match field_kind_repr kind with
+      Fvar _ (* {contents = None} *) -> print_string "private "
+    | _ (* Fpresent *)               -> ()
+    end;
+    if not (Concr.mem lab concrete) then print_string "virtual ";
+    print_string lab;
+    print_string " :";
+    print_space ();
+    typexp sch 0 ty;
+    close_box ()
+  end
 
-let methods_of_type ty =
-  match (repr ty).desc with
-    Tobject (m, _) -> m
-  | _              -> fatal_error "Printtyp.methods_of_type"
+let rec prepare_class_type path =
+  function
+    Tcty_constr (p, rv::tyl, cty)
+        when not (Path.same p path) && (repr rv).desc = Tvar ->
+      let sty = Ctype.self_type cty in
+      visited_objects := sty :: !visited_objects;
+      List.iter mark_loops tyl
+  | Tcty_constr (_, _, cty)  ->
+      prepare_class_type path cty
+  | Tcty_signature sign ->
+      let sty = repr sign.cty_self in
+      (* Self may have a name *)
+      visited_objects := sty :: !visited_objects;
+      begin match sty.desc with
+        Tobject (fi, _) -> mark_loops fi
+      | _               -> assert false
+      end;
+      Vars.iter (fun _ (_, ty) -> mark_loops ty) sign.cty_vars
+  | Tcty_fun (ty, cty) ->
+      prepare_class_type path cty;
+      mark_loops ty
+
+let rec perform_class_type sch p params =
+  function
+    Tcty_constr (p', rv::tyl, cty)
+(* XXX Critere de non-expansion insuffisant :
+   expanser egalement s'il y a plus de methods publiques *)
+        when not (Path.same p p') && (repr rv).desc = Tvar ->
+      let sty = Ctype.self_type cty in
+      open_box 0;
+      if tyl <> [] then begin
+        open_box 1;
+        print_string "[";
+        typlist true 0 "," tyl;
+        print_string "]";
+        close_box ();
+        print_space ()
+      end;
+      path p';
+      if List.memq sty !aliased then begin
+        print_space ();
+        open_box 0;
+        print_string "['";
+        print_string (name_of_type sty);
+        print_string "]";
+        close_box ()
+      end;
+      close_box ()
+  | Tcty_constr (_, _, cty)  ->
+      perform_class_type sch p params cty
+  | Tcty_signature sign ->
+      let sty = repr sign.cty_self in
+      open_hvbox 2;
+      open_box 2;
+      print_string "sig";
+      if List.memq sty !aliased then begin
+        print_space ();
+        open_box 0;
+        print_string "('";
+        print_string (name_of_type sty);
+        print_string ")";
+        close_box ()
+      end;
+      close_box ();
+      List.iter constrain params;
+      Vars.iter (class_var sch) sign.cty_vars;
+      let (fields, _) =
+        Ctype.flatten_fields (Ctype.object_fields sign.cty_self)
+      in
+      List.iter (metho sch sign.cty_concr) fields;
+      print_break 1 (-2);
+      print_string "end";
+      close_box()
+  | Tcty_fun (ty, cty) ->
+      open_box 0;
+      print_string "{"; typexp sch 0 ty; print_string "} ->";
+      print_space ();
+      perform_class_type sch p params cty;
+      close_box ()
 
-let rec list_public_methods ty =
-  let (fields, _) = flatten_fields ty in
-  List.map (function (m, _, t) -> (m, t)) fields
+let rec alternate_class_type sch path params cty =
+  match cty with
+    Tcty_signature _ | Tcty_constr _ ->
+      print_string ":"; print_space ();
+      perform_class_type sch path params cty
+  | Tcty_fun (ty, cty) ->
+      print_string "("; typexp sch 0 ty; print_string ")";
+      print_space ();
+      alternate_class_type sch path params cty
+
+let class_type cty =
+  reset ();
+  let no_path = Pident (Ident.create "") in
+  prepare_class_type no_path cty;
+  perform_class_type false no_path [] cty
 
-let class_type id cl_ty =
-  let self = repr cl_ty.cty_self in
-  let params = List.map repr cl_ty.cty_params in
-  let args = cl_ty.cty_args in
-  let vars = cl_ty.cty_vars in
+let class_declaration id cl =
+  let params = List.map repr cl.cty_params in
 
   reset ();
-  (* Self may have a name *)
-  visited_objects := self :: !visited_objects;
   aliased := params @ !aliased;
-  begin match self.desc with
-    Tobject (fi, _) -> mark_loops fi
-  | _               -> fatal_error "Printtyp.class_type"
-  end;
+  prepare_class_type cl.cty_path cl.cty_type;
+  let sty = self_type cl.cty_type in
   List.iter mark_loops params;
-  List.iter mark_loops args;
-  Vars.iter (fun _ (_, ty) -> mark_loops ty) vars;
-  Meths.iter (fun _ ty -> mark_loops ty) cl_ty.cty_meths;
+
   List.iter (fun x -> name_of_type x; ()) params;
-  open_hvbox 2;
-  open_box 0;
-  print_string "class ";
-  if cl_ty.cty_new = None then
-    print_string "virtual ";
-  if not (opened_object self) then
-    print_string "closed ";
-  type_sch {desc = Tconstr(Pident id, params, ref Mnil); level = 0};
-  if List.memq self !aliased then
-    (name_of_type self; ());
-  List.iter class_arg args;
-  if List.memq self !aliased then begin
-    print_string " : ";
-    print_string "'";
-    print_string (name_of_type self)
+  if List.memq sty !aliased then
+    (name_of_type sty; ());
+
+  open_box 2;
+  print_string "class";
+  print_space ();
+  if cl.cty_new = None then begin
+    print_string "virtual";
+    print_space ()
   end;
-  print_string " =";
-  close_box ();
-  List.iter constrain params;
-  Vars.iter class_var vars;
-  let public_methods = list_public_methods (methods_of_type self) in
-  let methods =
-    List.fold_left (fun m (lab, ty) -> Meths.add lab ty m)
-      cl_ty.cty_meths public_methods
+  if params <> [] then begin
+    open_box 1;
+    print_string "[";
+    typlist true 0 "," params;
+    print_string "]";
+    close_box ();
+    print_space ()
+  end;
+  ident id;
+  print_space ();
+  alternate_class_type true cl.cty_path params cl.cty_type;
+  close_box ()
+
+let cltype_declaration id cl =
+  let params = List.map repr cl.clty_params in
+
+  reset ();
+  aliased := params @ !aliased;
+  prepare_class_type cl.clty_path cl.clty_type;
+  let sty = self_type cl.clty_type in
+  List.iter mark_loops params;
+
+  List.iter (fun x -> name_of_type x; ()) params;
+  if List.memq sty !aliased then
+    (name_of_type sty; ());
+
+  let sign = Ctype.signature_of_class_type cl.clty_type in
+  let virt =
+    let (fields, _) =
+      Ctype.flatten_fields (Ctype.object_fields sign.cty_self)
+    in
+    List.exists
+      (fun (lab, _, ty) ->
+         not ((lab = "*dummy method*")
+                         ||
+              (Concr.mem lab sign.cty_concr)))
+      fields
   in
-  Meths.iter (metho public_methods cl_ty.cty_concr) methods;
-  print_break 1 (-2);
-  print_string "end";
-  close_box()
+
+  open_box 2;
+  print_string "class type";
+  print_space ();
+  if virt then begin
+    print_string "virtual";
+    print_space ()
+  end;
+  if params <> [] then begin
+    open_box 1;
+    print_string "[";
+    typlist true 0 "," params;
+    print_string "]";
+    close_box ();
+    print_space ()
+  end;
+  ident id;
+  print_space ();
+  print_string "=";
+  print_space ();
+  perform_class_type true cl.clty_path params cl.clty_type;
+  close_box ()
 
 (* Print a module type *)
 
@@ -535,8 +654,13 @@ and signature_body spc = function
         | Tsig_modtype(id, decl)  ->
             modtype_declaration id decl; rem
         | Tsig_class(id, decl) ->
-            class_type id decl;
-            match rem with tydecl1 :: tydecl2 :: rem -> rem | _ -> []
+            class_declaration id decl;
+            begin match rem with
+              ctydecl::tydecl1::tydecl2::rem -> rem | _ -> []
+            end
+        | Tsig_cltype(id, decl) ->
+            cltype_declaration id decl;
+            match rem with tydecl1::tydecl2::rem -> rem | _ -> []
       in signature_body true cont
 
 and modtype_declaration id decl =
@@ -585,18 +709,68 @@ let rec trace fst txt =
   | _ ->
       ()
 
+let rec mismatch =
+  function
+    [(_, t); (_, t')] -> (t, t')
+  | _ :: _ :: rem     -> mismatch rem
+  | _                 -> assert false
+
+let rec filter_trace =
+  function
+    (t1, t1')::(t2, t2')::rem ->
+      let rem' = filter_trace rem in
+      if (t1 == t1') & (t2 == t2')
+      then rem'
+      else (t1, t1')::(t2, t2')::rem'
+  | _ ->
+      []
+
 let unification_error tr txt1 txt2 =
   reset ();
-  List.iter
-    (function (t, t') -> mark_loops t; if t != t' then mark_loops t')
-    tr;
-  open_box 0;
-  let (t1, t1') = List.hd tr in
-  let (t2, t2') = List.hd (List.tl tr) in
-  txt1 (); print_break 1 2;
-  type_expansion t1 t1'; print_space();
-  txt2 (); print_break 1 2;
-  type_expansion t2 t2';
-  close_box();
-  trace false (fun _ -> print_string "is not compatible with type")
-        (List.tl (List.tl tr))
+  let (t3, t4) = mismatch tr in
+  match tr with
+    [] | _::[] ->
+      assert false
+  | (t1, t1')::(t2, t2')::tr ->
+      let tr = filter_trace tr in
+      let mark (t, t') = mark_loops t; if t != t' then mark_loops t' in
+      mark (t1, t1'); mark (t2, t2');
+      List.iter mark tr;
+      open_box 0;
+      txt1 (); print_break 1 2;
+      type_expansion t1 t1'; print_space();
+      txt2 (); print_break 1 2;
+      type_expansion t2 t2';
+      close_box();
+      trace false (fun _ -> print_string "is not compatible with type") tr;
+      print_cut ();
+      match t3.desc, t4.desc with
+        Tfield _, Tvar | Tvar, Tfield _ ->
+          print_string "Self type cannot escape its class"
+      | Tconstr (p, _, _), Tvar ->
+          open_box 0;
+          print_string "The type constructor"; print_break 1 2;
+          path p;
+          print_space (); print_string "would escape its scope";
+          close_box()
+      | Tvar, Tconstr (p, _, _) ->
+          open_box 0;
+          print_string "The type constructor"; print_break 1 2;
+          path p;
+          print_space (); print_string "would escape its scope";
+          close_box()
+      | Tfield ("*dummy method*", _, _, _), _
+      | _, Tfield ("*dummy method*", _, _, _) ->
+          print_string "Self type cannot be unified with a closed object type"
+      | Tfield (l, _, _, _), _ ->
+          open_box 0;
+          print_string "Only the first object type has a method ";
+          print_string l;
+          close_box()
+      | _, Tfield (l, _, _, _) ->
+          open_box 0;
+          print_string "Only the second object type has a method ";
+          print_string l;
+          close_box()
+      | _ ->
+          ()
diff --git a/typing/printtyp.mli b/typing/printtyp.mli
index c51a2be2fb..23c4e088bd 100644
--- a/typing/printtyp.mli
+++ b/typing/printtyp.mli
@@ -29,7 +29,9 @@ val modtype: module_type -> unit
 val signature: signature -> unit
 val signature_body: bool -> signature -> unit
 val modtype_declaration: Ident.t -> modtype_declaration -> unit
-val class_type: Ident.t -> class_type -> unit
+val class_type: class_type -> unit
+val class_declaration: Ident.t -> class_declaration -> unit
+val cltype_declaration: Ident.t -> cltype_declaration -> unit
 val type_expansion: type_expr -> type_expr -> unit
 val trace: bool -> (unit -> unit) -> (type_expr * type_expr) list -> unit
 val unification_error:
diff --git a/typing/subst.ml b/typing/subst.ml
index ba036f4a49..221c3a7891 100644
--- a/typing/subst.ml
+++ b/typing/subst.ml
@@ -102,8 +102,10 @@ let rec typexp s ty =
           begin match field_kind_repr kind with
             Fpresent ->
               Tfield(label, Fpresent, typexp s t1, typexp s t2)
-          | _ ->
-              Tlink(typexp s t2)
+          | Fabsent ->
+              Tlink (typexp s t2)
+          | Fvar _ (* {contents = None} *) as k ->
+              Tfield(label, k, typexp s t1, typexp s t2)
           end
       | Tnil ->
           Tnil
@@ -145,28 +147,28 @@ let type_declaration s decl =
     }
   in
   cleanup_types ();
-  List.iter unmark_type decl.type_params;
-  begin match decl.type_kind with
-    Type_abstract -> ()
-  | Type_variant cstrs ->
-      List.iter (fun (c, tl) -> List.iter unmark_type tl) cstrs
-  | Type_record lbls ->
-      List.iter (fun (c, mut, t) -> unmark_type t) lbls
-  end;
-  begin match decl.type_manifest with
-    None    -> ()
-  | Some ty -> unmark_type ty
-  end;
+  unmark_type_decl decl;
   decl
 
-let class_type s decl =
+let class_signature s sign =
+  { cty_self = typexp s sign.cty_self;
+    cty_vars = Vars.map (function (m, t) -> (m, typexp s t)) sign.cty_vars;
+    cty_concr = sign.cty_concr }
+
+let rec class_type s =
+  function
+    Tcty_constr (p, tyl, cty) ->
+      Tcty_constr (type_path s p, List.map (typexp s) tyl, class_type s cty)
+  | Tcty_signature sign ->
+      Tcty_signature (class_signature s sign)
+  | Tcty_fun (ty, cty) ->
+      Tcty_fun (typexp s ty, class_type s cty)
+
+let class_declaration s decl =
   let decl =
     { cty_params = List.map (typexp s) decl.cty_params;
-      cty_args = List.map (typexp s) decl.cty_args;
-      cty_vars = Vars.map (function (m, t) -> (m, typexp s t)) decl.cty_vars;
-      cty_meths = Meths.map (typexp s) decl.cty_meths;
-      cty_self = typexp s decl.cty_self;
-      cty_concr = decl.cty_concr;
+      cty_type = class_type s decl.cty_type;
+      cty_path = type_path s decl.cty_path;
       cty_new =
         begin match decl.cty_new with
           None    -> None
@@ -175,16 +177,30 @@ let class_type s decl =
   in
   cleanup_types ();
   List.iter unmark_type decl.cty_params;
-  List.iter unmark_type decl.cty_args;
-  Vars.iter (fun l (m, t) -> unmark_type t) decl.cty_vars;
-  Meths.iter (fun l t -> unmark_type t) decl.cty_meths;
-  unmark_type decl.cty_self;
+  unmark_class_type decl.cty_type;
   begin match decl.cty_new with
     None    -> ()
   | Some ty -> unmark_type ty
   end;
   decl
 
+let cltype_declaration s decl =
+  let decl =
+    { clty_params = List.map (typexp s) decl.clty_params;
+      clty_type = class_type s decl.clty_type;
+      clty_path = type_path s decl.clty_path }
+  in
+  cleanup_types ();
+  List.iter unmark_type decl.clty_params;
+  unmark_class_type decl.clty_type;
+  decl
+
+let class_type s cty =
+  let cty = class_type s cty in
+  cleanup_types ();
+  unmark_class_type cty;
+  cty
+
 let value_description s descr =
   { val_type = type_expr s descr.val_type;
     val_kind = descr.val_kind }
@@ -221,7 +237,9 @@ and signature s = function
       Tsig_modtype(id, modtype_declaration s d) ::
       signature (remove_modtype id s) sg
   | Tsig_class(id, d) :: sg ->
-      Tsig_class(id, class_type s d) :: signature s sg
+      Tsig_class(id, class_declaration s d) :: signature s sg
+  | Tsig_cltype(id, d) :: sg ->
+      Tsig_cltype(id, cltype_declaration s d) :: signature s sg
 
 and modtype_declaration s = function
     Tmodtype_abstract -> Tmodtype_abstract
diff --git a/typing/subst.mli b/typing/subst.mli
index cd60d886dc..ca5be84a81 100644
--- a/typing/subst.mli
+++ b/typing/subst.mli
@@ -36,11 +36,13 @@ val add_module: Ident.t -> Path.t -> t -> t
 val add_modtype: Ident.t -> module_type -> t -> t
 
 val type_expr: t -> type_expr -> type_expr
+val class_type: t -> class_type -> class_type
 val value_description: t -> value_description -> value_description
 val type_declaration: t -> type_declaration -> type_declaration
 val exception_declaration:
         t -> exception_declaration -> exception_declaration
-val class_type: t -> class_type -> class_type
+val class_declaration: t -> class_declaration -> class_declaration
+val cltype_declaration: t -> cltype_declaration -> cltype_declaration
 val modtype: t -> module_type -> module_type
 val signature: t -> signature -> signature
 val modtype_declaration: t -> modtype_declaration -> modtype_declaration
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index 42131393e5..22c49daf09 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -20,1169 +20,921 @@ open Typecore
 open Typetexp
 
 type error =
-    Duplicate_method of string
-  | Duplicate_variable of string
-  | Duplicate_super_variable of string
-  | Repeated_parameter
-  | Virtual_class of string * string
-  | Closed_class of string
-  | Closed_ancestor of string * Path.t * string
-  | Non_generalizable of Ident.t * type_expr list
-  | Non_closed of Ident.t * type_expr list * type_expr *
-                  Ctype.closed_schema_result
-  | Mutable_var of string
-  | Undefined_var of string
-  | Variable_type_mismatch of string * (type_expr * type_expr) list
+    Unconsistent_constraint of (type_expr * type_expr) list
   | Method_type_mismatch of string * (type_expr * type_expr) list
-  | Unconsistent_constraint
+  | Structure_expected of class_type
+  | Cannot_apply of class_type
+  | Pattern_type_clash of type_expr
+  | Repeated_parameter
   | Unbound_class of Longident.t
-  | Argument_type_mismatch of (type_expr * type_expr) list
+  | Unbound_class_2 of Longident.t
+  | Unbound_class_type of Longident.t
+  | Unbound_class_type_2 of Longident.t
   | Abbrev_type_clash of type_expr * type_expr * type_expr
-  | Bad_parameters of Ident.t * type_expr * type_expr
-  | Illdefined_class of string
-  | Argument_arity_mismatch of Path.t * int * int
-  | Parameter_arity_mismatch of Path.t * int * int
+  | Constructor_type_mismatch of string * (type_expr * type_expr) list
+  | Virtual_class of bool * string list
+  | Parameter_arity_mismatch of Longident.t * int * int
   | Parameter_mismatch of (type_expr * type_expr) list
+  | Bad_parameters of Ident.t * type_expr * type_expr
+  | Class_match_failure of Ctype.class_match_failure list
+  | Unbound_val of string
+  | Unbound_type_var of (unit -> unit) * Ctype.closed_class_failure
+  | Make_nongen_seltype of type_expr
 
 exception Error of Location.t * error
 
 
-                              (*****************)
-                              (*  Common code  *)
-                              (*****************)
+                       (**********************)
+                       (*  Useful constants  *)
+                       (**********************)
+                                   
 
+(*
+   Self type have a dummy private method, thus preventing it to become
+   closed.
+*)
+let dummy_method = "*dummy method*"
 
-let rec iter f env =
+(*
+   Path associated to the temporary class type of a class being typed
+   (its constructor is not available).
+*)
+let unbound_class = Path.Pident (Ident.create "")
+
+
+                (************************************)
+                (*  Some operations on class types  *)
+                (************************************)
+                                   
+
+(* Fully expand the head of a class type *)
+let rec scrape_class_type =
   function
-    [] ->
-      ([], env)
-  | cl :: cl_rem ->
-      let (cl', env') = f env cl in
-      let (cl_rem', env'') = iter f env' cl_rem in
-      (cl'::cl_rem', env'')
-
-let check_mutable loc lab mut mut' =
-  match mut, mut' with
-    (Immutable, Mutable) ->
-      raise(Error(loc, Mutable_var lab))
-  | _ ->
-      ()
+    Tcty_constr (_, _, cty) -> scrape_class_type cty
+  | cty                     -> cty
 
-let rec add_methods env self t =
-  match (Ctype.repr t).desc with
-    Tfield (lab, k, _, t') ->
-      if Btype.field_kind_repr k = Fpresent then begin
-        Ctype.filter_method env lab Public self; ()
-      end;
-      add_methods env self t'
-  | _ ->
-      ()
-
-(* Make sure that [self] has at least the methods of [obj]. *)
-let equalize_methods env self obj =
-  match (Ctype.expand_head env obj).desc with
-    Tobject (ty, _) ->
-      let rec equalize_methods_rec t =
-        match (Ctype.repr t).desc with
-          Tfield (lab, k, _, t') ->
-            if Btype.field_kind_repr k = Fpresent then begin
-              Ctype.filter_method env lab Public self; ()
-            end;
-            equalize_methods_rec t'
-        | _ ->
-            ()
-      in
-        equalize_methods_rec ty
-  | _ ->
-      fatal_error "Typeclass.equalize_methods"
+(* Generalize a class type *)
+let rec generalize_class_type =
+  function
+    Tcty_constr (_, params, cty) ->
+      List.iter Ctype.generalize params;
+      generalize_class_type cty
+  | Tcty_signature {cty_self = sty; cty_vars = vars } ->
+      Ctype.generalize sty;
+      Vars.iter (fun _ (_, ty) -> Ctype.generalize ty) vars
+  | Tcty_fun (ty, cty) ->
+      Ctype.generalize ty;
+      generalize_class_type cty
+
+(* Return the virtual methods of a class type *)
+let virtual_methods cty =
+  let sign = Ctype.signature_of_class_type cty in
+  let (fields, _) = Ctype.flatten_fields (Ctype.object_fields sign.cty_self) in
+  List.fold_left
+    (fun virt (lab, _, _) ->
+       if lab = dummy_method then virt else
+       if Concr.mem lab sign.cty_concr then virt else
+       lab::virt)
+    [] fields
+
+(* Return the constructor type associated to a class type *)
+let rec constructor_type constr cty =
+  match cty with
+    Tcty_constr (_, _, cty) ->
+      constructor_type constr cty
+  | Tcty_signature sign ->
+      constr
+  | Tcty_fun (ty, cty) ->
+      Ctype.newty (Tarrow (ty, constructor_type constr cty))
+
+let rec class_body cty =
+  match cty with
+    Tcty_constr (_, _, cty) ->
+      class_body cty
+  | Tcty_signature sign ->
+      cty
+  | Tcty_fun (ty, cty) ->
+      class_body cty
+
+let rec extract_constraints cty =
+  let sign = Ctype.signature_of_class_type cty in
+  (Vars.fold (fun lab _ vars -> lab :: vars) sign.cty_vars [],
+   begin let (fields, _) =
+     Ctype.flatten_fields (Ctype.object_fields sign.cty_self)
+   in
+   List.fold_left
+     (fun meths (lab, _, _) ->
+        if lab = dummy_method then meths else lab::meths)
+     [] fields
+   end,
+   sign.cty_concr)
+
+
+                (***********************************)
+                (*  Primitives for typing classes  *)
+                (***********************************)
+                                   
+
+(* Enter a value in the method environment only *)
+let enter_met_env lab kind ty val_env met_env par_env =
+  let (id, val_env) =
+    Env.enter_value lab {val_type = ty; val_kind = Val_unbound} val_env
+  in
+  (id, val_env,
+   Env.add_value id {val_type = ty; val_kind = kind} met_env,
+   Env.add_value id {val_type = ty; val_kind = Val_unbound} par_env)
+
+(* Enter an instance variable in the environment *)
+let enter_val vars lab mut ty val_env met_env par_env =
+  let (id, val_env, met_env, par_env) as result =
+    enter_met_env lab (Val_ivar mut) ty val_env met_env par_env
+  in
+  vars := Vars.add lab (id, mut, ty) !vars;
+  result
 
+let rec make_nongen_class_type env =
+  function
+    Tcty_constr (_, _, cty) ->
+      make_nongen_class_type env cty
+  | Tcty_signature sign ->
+      Vars.iter (fun _ (_, ty) -> Ctype.make_nongen ty) sign.cty_vars;
+      Concr.iter
+        (function nm ->
+           Ctype.make_nongen
+            (Ctype.filter_method env nm Private sign.cty_self))
+        sign.cty_concr
+  | Tcty_fun (ty, cty) ->
+      Ctype.make_nongen ty;
+      make_nongen_class_type env cty
+
+let inheritance impl self_type env concr_meths loc parent =
+  match scrape_class_type parent with
+    Tcty_signature cl_sig ->
 
-let rec type_meth env loc self ty =
-  match (Ctype.repr ty).desc with
-    Tfield (lab, k, ty, ty') ->
-      if Btype.field_kind_repr k = Fpresent then begin
-        let ty0 = Ctype.filter_method env lab Public self in
-        begin try
-          Ctype.unify env ty ty0
-        with Ctype.Unify trace ->
-          raise(Error(loc, Method_type_mismatch (lab, trace)))
+      (* Methods *)
+      begin try
+        Ctype.unify env self_type cl_sig.cty_self
+      with Ctype.Unify trace ->
+        match trace with
+          _::_::_::({desc = Tfield(n, _, _, _)}, _)::rem ->
+            raise(Error(loc, Method_type_mismatch (n, rem)))
+        | _ ->
+            assert false
+      end;
+
+      if impl then begin
+        let overridings = Concr.inter cl_sig.cty_concr concr_meths in
+        if not (Concr.is_empty overridings) then begin
+          Location.print_warning loc
+            ("the following methods are overriden by the inherited class:\n  "
+               ^ (String.concat " " (Concr.elements overridings)))
         end
       end;
-      type_meth env loc self ty'
-  | _ ->
-      ()
+      let concr_meths = Concr.union cl_sig.cty_concr concr_meths in
 
-let vals_remove lab vals =
-  Vars.fold (fun l k v -> if lab = l then v else Vars.add l k v)
-    vals Vars.empty
+      (cl_sig, concr_meths)
 
-let insert_value env lab priv mut ty loc vals =
-  begin try
-    let (mut', ty') = Vars.find lab vals in
-    check_mutable loc lab mut mut';
-    try Ctype.unify env ty ty' with Ctype.Unify trace ->
-      raise(Error(loc, Variable_type_mismatch(lab, trace)))
-  with Not_found -> () end;
-  if priv = Private then
-    vals_remove lab vals
-  else
-    Vars.add lab (mut, ty) vals
-
-let rec closed_scheme t =
-  match (Ctype.repr t).desc with
-    Tfield (lab, k, _, t') when Btype.field_kind_repr k = Fpresent ->
-      Ctype.newty (Tfield (lab, Fpresent, Ctype.newvar (), closed_scheme t'))
-  | Tfield (lab, _, _, t') ->
-      closed_scheme t'
-  | Tnil ->
-      Ctype.newty Tnil
   | _ ->
-      fatal_error "Typeclass.closed_scheme"
-
-let change_value_status lab priv mut loc vals =
-  try
-    let (mut', ty') = Vars.find lab vals in
-    check_mutable loc lab mut mut';
-    if priv = Private then
-      (vals_remove lab vals, ty')
-    else
-      (Vars.add lab (mut, ty') vals, ty')
-  with Not_found ->
-    raise(Error(loc, Undefined_var lab))
-
-let missing_method env ty ty' =
-  let rec missing_method_rec met=
-    match (Ctype.repr met).desc with
-      Tfield(lab, k, _, met') ->
-        begin try
-          if Btype.field_kind_repr k = Fpresent then begin
-            Ctype.filter_method env lab Public ty; ()
-          end;
-          missing_method_rec met'
-        with Ctype.Unify _ ->
-          lab
-        end
-    | _ ->
-        fatal_error "Typeclass.missing_method (1)"
-  in
-  match (Ctype.expand_head env ty').desc with
-    Tobject (met, _) ->
-      missing_method_rec met
-  | _ ->
-      fatal_error "Typeclass.missing_method (2)"
-
-let generalize_class cl_sig =
-  List.iter Ctype.generalize cl_sig.cty_params;
-  List.iter Ctype.generalize cl_sig.cty_args;
-  Vars.iter (fun l (m, t) -> Ctype.generalize t) cl_sig.cty_vars;
-  Meths.iter (fun l t -> Ctype.generalize t) cl_sig.cty_meths;
-  Ctype.generalize cl_sig.cty_self;
-  match cl_sig.cty_new with Some ty -> Ctype.generalize ty | None -> ()
-
-
-                              (***********************)
-                              (*  Class translation  *)
-                              (***********************)
-
-
-let make_stub env (cl, obj_id, cl_id) =
-  Ctype.begin_def ();
-
-  (* Create self (class type) *)
-  let self = Ctype.newobj (Ctype.newvar ()) in
-
-  (* Find concrete methods and marks methods *)
-  let concr_meths =
-    List.fold_left
-      (function meths ->
-         function
-           Pcf_inher (nm, _, _, _, loc) ->
-             let (_, anc) =
-               try
-                 Env.lookup_class nm env
-               with Not_found ->
-                 raise(Error(loc, Unbound_class nm))
-             in
-               begin match (Ctype.expand_head env anc.cty_self).desc with
-                 Tobject (ty, _) ->
-                   add_methods env self ty;
-                   Concr.union anc.cty_concr meths
-               | _ -> fatal_error "Typeclass.make_stub"
-               end
-         | Pcf_val _ ->
-             meths
-         | Pcf_virt (lab, priv, _, _) ->
-             Ctype.filter_method env lab priv self;
-             meths
-         | Pcf_meth (lab, priv, _, _) ->
-             Ctype.filter_method env lab priv self;
-             Concr.add lab meths)
-      Concr.empty cl.pcl_field
-  in
-
-  Ctype.end_def ();
-  Ctype.generalize self;
+      raise(Error(loc, Structure_expected parent))
 
-  (* Temporary object type *)
-  let temp_obj_params =
-    List.map (fun _ -> Ctype.newvar ()) (fst cl.pcl_param)
-  in
-  let temp_obj = Ctype.instance self in
-  let obj_temp_abbrev =
-    { type_params = temp_obj_params;
-      type_arity = List.length temp_obj_params;
-      type_kind = Type_abstract;
-      type_manifest = Some temp_obj }
-  in let temp_env = Env.add_type obj_id obj_temp_abbrev env
-  in let abbrev =
-    Ctype.newty (Tconstr (Path.Pident obj_id, temp_obj_params, ref Mnil))
+let virtual_method val_env meths self_type lab priv sty loc =
+  let (_, ty') =
+     Ctype.filter_self_method val_env lab priv meths self_type
   in
+  let ty = transl_simple_type val_env false sty in
+  try Ctype.unify val_env ty ty' with Ctype.Unify trace ->
+    raise(Error(loc, Method_type_mismatch (lab, trace)))
 
-  (* Temporary class type *)
-  let (temp_cl_params, temp_cl) =
-    if cl.pcl_closed = Closed then
-      (temp_obj_params,
-       Ctype.newty (Tconstr(Path.Pident obj_id, temp_obj_params, ref Mnil)))
-    else begin
-      let params = List.map (fun _ -> Ctype.newvar ()) (fst cl.pcl_param) in
-      let ty = Ctype.instance self in
-      Ctype.set_object_name ty params obj_id;
-      (params, ty)
-    end
-  in
-  let cl_temp_abbrev =
-    { type_params = temp_cl_params;
-      type_arity = List.length temp_cl_params;
-      type_kind = Type_abstract;
-      type_manifest = Some temp_cl }
-  in let temp_env = Env.add_type cl_id cl_temp_abbrev temp_env
-  in let cl_abbrev =
-    Ctype.newty (Tconstr (Path.Pident cl_id, temp_cl_params, ref Mnil))
-  in
+let type_constraint val_env sty sty' loc =
+  let ty  = transl_simple_type val_env false sty in
+  let ty' = transl_simple_type val_env false sty' in
+  try Ctype.unify val_env ty ty' with Ctype.Unify trace ->
+    raise(Error(loc, Unconsistent_constraint trace))
 
-  (* Temporary type for new *)
-  let new_args = List.map (fun _ -> Ctype.newvar ()) cl.pcl_args in
-  let new_ty =
-    if cl.pcl_kind = Concrete then
-      Some (List.fold_right
-              (fun arg ty -> Ctype.newty (Tarrow(arg, ty)))
-              new_args abbrev)
-    else
-      None  
-  in let cl_temp_sig =
-    { cty_params = [];
-      cty_args = []; cty_vars = Vars.empty;
-      cty_meths = Meths.empty;
-      cty_self = self; cty_concr = concr_meths;
-      cty_new = new_ty }
-  in let (id, temp_env) = Env.enter_class cl.pcl_name cl_temp_sig temp_env in
-
-  ((cl, id, cl_id, obj_id, self, concr_meths, new_args, new_ty,
-    temp_cl, temp_cl_params, cl_abbrev, temp_obj, temp_obj_params, abbrev),
-   temp_env)
-
-let type_class_field env var_env self cl
-    (met_env, fields, vars_sig, meths) =
+(*******************************)
+
+let rec class_type_field env self_type meths (val_sig, concr_meths) =
   function
-    Pcf_inher (cl_name, params, args, super, loc) ->
-      (* Find class type *)
-      let (path, cl_type) =
-        try
-          Env.lookup_class cl_name env
-        with Not_found ->
-          raise(Error(loc, Unbound_class cl_name))
+    Pctf_inher sparent ->
+      let parent = class_type env sparent in
+      let (cl_sig, concr_meths) =
+        inheritance false self_type env concr_meths sparent.pcty_loc parent
       in
-      let (params', args', vars', meths', self') =
-        Ctype.instance_class cl_type
+      let val_sig =
+        Vars.fold
+          (fun lab (mut, ty) val_sig -> Vars.add lab (mut, ty) val_sig)
+          cl_sig.cty_vars val_sig
+      in
+      (val_sig, concr_meths)
+
+  | Pctf_val (lab, mut, sty_opt, loc) ->
+      let (mut, ty) =
+        match sty_opt with
+          None     ->
+            let (mut', ty) =
+              try Vars.find lab val_sig with Not_found ->
+                raise(Error(loc, Unbound_val lab))
+            in
+            (if mut = Mutable then mut' else Immutable), ty
+        | Some sty ->
+            mut, transl_simple_type env false sty
       in
+      (Vars.add lab (mut, ty) val_sig, concr_meths)
 
-      (* Unify parameters *)
-      if List.length params <> List.length params' then
-        raise(Error(loc, Parameter_arity_mismatch
-                    (path, List.length params', List.length params)));
+  | Pctf_virt (lab, priv, sty, loc) ->
+      virtual_method env meths self_type lab priv sty loc;
+      (val_sig, concr_meths)
+
+  | Pctf_meth (lab, priv, sty, loc)  ->
+      virtual_method env meths self_type lab priv sty loc;
+      (val_sig, Concr.add lab concr_meths)
+
+  | Pctf_cstr (sty, sty', loc) ->
+      type_constraint env sty sty' loc;
+      (val_sig, concr_meths)
+
+and class_signature env sty sign =
+  let meths = ref Meths.empty in
+  let self_type = transl_simple_type env false sty in
+  
+  (* Check that the binder is a correct type, and introduce a dummy
+     method preventing self type from being closed. *)
+  begin try
+    Ctype.filter_method env dummy_method Private self_type
+  with Ctype.Unify _ ->
+    raise(Error(sty.ptyp_loc, Pattern_type_clash self_type))
+  end;
+  
+  (* Class type fields *)
+  let (val_sig, concr_meths) =
+    List.fold_left (class_type_field env self_type meths)
+      (Vars.empty, Concr.empty)
+      sign
+  in
+  
+  {cty_self = self_type;
+   cty_vars = val_sig;
+   cty_concr = concr_meths }
+
+and class_type env scty =
+  match scty.pcty_desc with
+    Pcty_constr (lid, styl) ->
+      let (path, decl) =
+        try Env.lookup_cltype lid env with Not_found ->
+          raise(Error(scty.pcty_loc, Unbound_class_type lid))
+      in
+      if Path.same decl.clty_path unbound_class then
+        raise(Error(scty.pcty_loc, Unbound_class_type_2 lid));
+      let (params, clty) =
+        Ctype.instance_class decl.clty_params decl.clty_type
+      in
+      let sty = Ctype.self_type clty in
+(* XXX Usage incorrect de Ctype.row_variable *)
+      let rv = Ctype.row_variable sty in
+      if List.length params <> List.length styl then
+        raise(Error(scty.pcty_loc,
+                    Parameter_arity_mismatch (lid, List.length params,
+                                                   List.length styl)));
       List.iter2
         (fun sty ty ->
-           let ty' = Typetexp.transl_simple_type var_env false sty in
-           try Ctype.unify var_env ty' ty with Ctype.Unify trace ->
+           let ty' = transl_simple_type env false sty in
+           try Ctype.unify env ty' ty with Ctype.Unify trace ->
              raise(Error(sty.ptyp_loc, Parameter_mismatch trace)))
-        params params';
+        styl params;
+      Tcty_constr (path, rv::params, clty)
 
-      (* Type arguments *)
-      if List.length args <> List.length args' then
-        raise(Error(loc, Argument_arity_mismatch
-                        (path, List.length args', List.length args)));
-      let args = List.map2 (type_expect var_env) args args' in
+  | Pcty_signature (sty, sign) ->
+      Tcty_signature (class_signature env sty sign)
+      
+  | Pcty_fun (sty, scty) ->
+      let ty = transl_simple_type env false sty in
+      let cty = class_type env scty in
+      Tcty_fun (ty, cty)
 
+(*******************************)
+
+let rec class_field self_type meths vars
+    (val_env, met_env, par_env, fields, concr_meths) =
+  function
+    Pcf_inher (sparent, super) ->
+      let parent = class_expr val_env par_env sparent in
+      let (cl_sig, concr_meths) =
+        inheritance true self_type val_env concr_meths sparent.pcl_loc
+          parent.cl_type
+      in
       (* Variables *)
-      let (vars, vars_sig, met_env) =
+      let (val_env, met_env, par_env, inh_vars) =
         Vars.fold
-          (fun lab (mut, ty) (l, v_sig, env) ->
-             let (id, env) =
-               Env.enter_value lab
-                 {val_type = ty; val_kind = Val_ivar mut} env
+          (fun lab (mut, ty) (val_env, met_env, par_env, inh_vars) ->
+             let (id, val_env, met_env, par_env) =
+               enter_val vars lab mut ty val_env met_env par_env
              in
-             ((lab, id)::l,
-              insert_value var_env lab Public mut ty loc v_sig,
-              env))
-          vars' ([], vars_sig, met_env)
+             (val_env, met_env, par_env, (lab, id) :: inh_vars))
+          cl_sig.cty_vars (val_env, met_env, par_env, [])
       in
-
-      (* Methods *)
-      let meths =
-        Meths.fold
-          (fun lab ty m ->
-             let (id, ty') =
-               try Meths.find lab m with Not_found ->
-               (Ident.create lab,
-                Ctype.filter_method var_env lab Private self)
-             in
-             begin try Ctype.unify env ty ty' with Ctype.Unify trace ->
-               raise(Error(loc, Method_type_mismatch (lab, trace)))
-             end;
-             Meths.add lab (id, ty) m)
-          meths' meths
+      (* Inherited concrete methods *)
+      let inh_meths = 
+        Concr.fold (fun lab rem -> (lab, Ident.create lab)::rem)
+          cl_sig.cty_concr []
       in
-
-      (* Self type *)
-      let ty' = Ctype.expand_head var_env self' in
-      begin match ty'.desc with
-        Tobject (fi, _) ->
-          if not (Ctype.opened_object ty') then
-            begin try
-              Ctype.unify var_env self (Ctype.newobj (closed_scheme fi))
-            with Ctype.Unify _ ->
-              let lab = missing_method var_env ty' self in
-              raise(Error(loc, Closed_ancestor (cl.pcl_name, path, lab)))
-            end;
-          Ctype.unify var_env ty' self;
-          type_meth var_env loc self fi
-      | _ ->
-          fatal_error "Typeclass.transl_class"
-      end;
-
-      (* Super methods *)
-      let (met, met_env) =
+      (* Super *)      
+      let (val_env, met_env, par_env) =
         match super with
           None ->
-            ([], met_env)
+            (val_env, met_env, par_env)
         | Some name ->
-            let ty = Ctype.newobj (Ctype.newvar ()) in
-            let used_methods =
-              Concr.fold
-                (fun lab rem ->
-                   Ctype.unify met_env
-                     (Ctype.filter_method met_env lab Public ty)
-                     (Ctype.filter_method met_env lab Public self);
-                   (lab, Ident.create lab)::rem)
-                cl_type.cty_concr
-                []
-            in
-            Ctype.close_object ty;
-            let (id, met_env) =
-              Env.enter_value name
-                {val_type = ty; val_kind = Val_anc used_methods} met_env
+            let (id, val_env, met_env, par_env) =
+              enter_met_env name (Val_anc inh_meths) self_type
+                val_env met_env par_env
             in
-            (used_methods, met_env)
+            (val_env, met_env, par_env)
       in
-      let met' = Meths.fold (fun lab _ rem -> lab::rem) cl_type.cty_meths [] in
-      (met_env, Cf_inher (path, args, vars, met, met')::fields,
-       vars_sig, meths)
-
-  | Pcf_val (lab, priv, mut, sinit, loc) ->
-      begin match sinit with
-        Some sexp ->
-          let exp = type_exp var_env sexp in
-          let (id, met_env) =
-            Env.enter_value lab
-              {val_type = exp.exp_type; val_kind = Val_ivar mut} met_env
-          in
-          (met_env, Cf_val (lab, id, priv, Some exp)::fields,
-           insert_value var_env lab priv mut exp.exp_type loc vars_sig,
-           meths)
-      | None ->
-          let (vars_sig, ty) =
-            change_value_status lab priv mut loc vars_sig
-          in
-          let (id, met_env) =
-            Env.enter_value lab
-              {val_type = ty; val_kind = Val_ivar mut} met_env
-          in
-          (met_env, Cf_val (lab, id, priv, None)::fields, vars_sig, meths)
-      end
-
-  | Pcf_virt (lab, priv, ty, loc) ->
-      let ty = transl_simple_type met_env false ty in
-      let ty'' = Ctype.filter_method var_env lab priv self in
-      let (id, ty') =
-        try Meths.find lab meths with Not_found -> (Ident.create lab, ty'')
-      in
-      begin try Ctype.unify var_env ty ty'' with Ctype.Unify trace ->
-        raise(Error(loc, Method_type_mismatch (lab, trace)))
-      end;
-      (met_env, fields, vars_sig, Meths.add lab (id, ty) meths)
+      (val_env, met_env, par_env,
+       Cf_inher (parent, inh_vars, inh_meths)::fields, concr_meths)
 
-  | Pcf_meth (lab, priv, expr, loc)  ->
-      let ty' = Ctype.filter_method var_env lab priv self in
-      let (id, ty) =
-        try Meths.find lab meths with Not_found -> (Ident.create lab, ty')
+  | Pcf_val (lab, mut, sexp, loc) ->
+      let exp = type_exp val_env sexp in
+      if not (Typecore.is_nonexpansive exp) then
+        begin try
+          Ctype.make_nongen exp.exp_type
+        with Ctype.Unify [(ty, _)] ->
+          raise(Error(loc, Make_nongen_seltype ty))
+        end;
+      let (id, val_env, met_env, par_env) =
+        enter_val vars lab mut exp.exp_type val_env met_env par_env
       in
-      let meths = Meths.add lab (id, ty) meths in
-      let (texp, meths) = type_method met_env self cl.pcl_self meths expr ty in
-      (met_env, Cf_meth (lab, texp)::fields, vars_sig, meths)
-
-let transl_class temp_env env
-  (cl, id, cl_id, obj_id, self, concr_meths, new_args, new_ty,
-   temp_cl, temp_cl_params, cl_abbrev, temp_obj, temp_obj_params, abbrev)
-    =
-  reset_type_variables ();
-  Ctype.begin_def ();
-
-  (* Self type *)
-  let self = Ctype.instance self in
-
-  (* Introduce parameters *)
-  let params =
-    try
-      List.map (enter_type_variable true) (fst cl.pcl_param)
-    with Already_bound ->
-      raise(Error(snd cl.pcl_param, Repeated_parameter))
-  in
-
-  (* Translate constrained parameters *)
-  let cstr_params =
-    List.map (function (v, _, loc) -> type_variable loc v) cl.pcl_cstr
-  in
-
-  (* Bind self type variable *)
-  begin match cl.pcl_self_ty with
-      Some v -> Ctype.unify temp_env self (enter_type_variable false v)
-    | None   -> ()
-  end;
-
-  (* Add constraints *)
-  List.iter2
-    (fun (v, sty, loc) ty' ->
-       try
-         Ctype.unify temp_env (transl_simple_type temp_env false sty) ty'
-       with Ctype.Unify _ ->
-         raise(Error(loc, Unconsistent_constraint)))
-    cl.pcl_cstr cstr_params;
-
-  (* Type arguments and fields *)
-  let (args, var_env) = type_pattern_list temp_env cl.pcl_args in
-  let arg_sig = List.map (fun exp -> exp.pat_type) args in
-  let (_, fields, vars_sig, meths) =
-    List.fold_left (type_class_field env var_env self cl)
-      (temp_env, [], Vars.empty, Meths.empty)
-      cl.pcl_field
-  in
-
-  (* Closeness of self (1) *)
-  if cl.pcl_closed = Closed then
-    Ctype.close_object self;
-
-  (* Generalize class *)
-  Ctype.end_def ();
-  List.iter Ctype.generalize params;
-  List.iter Ctype.generalize arg_sig;
-  Vars.iter (fun l (m, t) -> Ctype.generalize t) vars_sig;
-  Meths.iter (fun l (i, t) -> Ctype.generalize t) meths;
-  Ctype.generalize self;
-
-  (* Temporary class abbreviation *)
-  let (cl_params, cl_ty) = Ctype.instance_parameterized_type params self in
-  begin try Ctype.unify temp_env temp_cl cl_ty with Ctype.Unify _ ->
-    Ctype.remove_object_name temp_cl;
-    raise(Error(cl.pcl_loc, Abbrev_type_clash (cl_abbrev, cl_ty, temp_cl)))
-  end;
-  begin try
-    List.iter2 (Ctype.unify temp_env) temp_cl_params cl_params
-  with Ctype.Unify _ ->
-    raise(Error(cl.pcl_loc,
-          Bad_parameters (cl_id, cl_abbrev,
-                          Ctype.newty (Tconstr (Path.Pident cl_id, cl_params,
-                                                ref Mnil)))))
-  end;
-
-  (* Object abbreviation and arguments for new *)
-  let (obj_params, arg_sig', obj_ty) =
-    Ctype.instance_parameterized_type_2 params arg_sig self
-  in
-  begin try Ctype.unify temp_env abbrev obj_ty with Ctype.Unify _ ->
-    raise(Error(cl.pcl_loc, Abbrev_type_clash (abbrev, obj_ty, temp_obj)))
-  end;
-  begin try
-    List.iter2 (Ctype.unify temp_env) temp_obj_params obj_params
-  with Ctype.Unify _ ->
-    raise(Error(cl.pcl_loc,
-          Bad_parameters (obj_id, abbrev,
-                          Ctype.newty (Tconstr (Path.Pident obj_id, obj_params,
-                                                ref Mnil)))))
-  end;
-  Ctype.close_object temp_obj;
-  List.iter2
-    (fun ty (exp, ty') ->
-       begin try
-         Ctype.unify temp_env ty' ty
-       with Ctype.Unify trace ->
-         raise(Error(exp.pat_loc, Argument_type_mismatch trace))
-       end)
-    new_args (List.combine args arg_sig');
-
-  (* Fill interface / implementation *)
-  let cl_imp =
-    { cl_args = args;
-      cl_field = List.rev fields;
-      cl_pub_meths = [];
-      cl_meths = Meths.map (function (id, ty) -> id) meths;
-      cl_loc = cl.pcl_loc }
-  in let cl_sig =
-    { cty_params = params;
-      cty_args = arg_sig;
-      cty_vars = vars_sig;
-      cty_meths = Meths.map (function (id, ty) -> ty) meths;
-      cty_self = self;
-      cty_concr = concr_meths;
-      cty_new = new_ty }
-  in let new_env = Env.add_class id cl_sig env in
-
-  ((cl, id, cl_id, obj_id, cl_sig, cl_imp, temp_obj,
-    temp_obj_params),
-   new_env)
-
-let build_new_type temp_env env
-  (cl, id, cl_id, obj_id, cl_sig, cl_imp, temp_obj,
-   temp_obj_params)
-    =
-  (* Modify constrainsts to ensure the object abbreviation is well-formed *)
-  let (params, args, vars, meths, self) = Ctype.instance_class cl_sig in
-  List.iter2 (Ctype.unify temp_env) params temp_obj_params;
-                                        (* Never fails *)
-
-  (* Hide private methods *)
-  Ctype.hide_private_methods cl_sig.cty_self;
-
-  (* Closeness of self (2) *)
-  if (cl.pcl_closed <> Closed) & not (Ctype.opened_object self) then
-    raise(Error(cl.pcl_loc, Closed_class cl.pcl_name));
-
-  equalize_methods temp_env self temp_obj;
-
-  (* self should not be an abbreviation (printtyp) *)
-  let exp_self = Ctype.expand_head temp_env self in
-
-  let public_methods =
-    match (Ctype.repr exp_self).desc with
-      Tobject (fi, _) ->
-        let (meths, _) = Ctype.flatten_fields fi in
-        List.map (function (lab, _, _) -> lab) meths
-    | _ -> fatal_error "Typeclass.build_new_type"
-  in
+      (val_env, met_env, par_env, Cf_val (lab, id, exp) :: fields, concr_meths)
 
-  (* Check whether the class can be concrete *)
-  if cl.pcl_kind = Concrete then begin
-    List.iter
-      (function m ->
-         if not (Concr.mem m cl_sig.cty_concr) then
-           raise(Error(cl.pcl_loc, Virtual_class (cl.pcl_name, m))))
-      public_methods;
-    Meths.iter
-      (fun m _ ->
-         if not (Concr.mem m cl_sig.cty_concr) then
-           raise(Error(cl.pcl_loc, Virtual_class (cl.pcl_name, m))))
-      meths
-  end;
+  | Pcf_virt (lab, priv, sty, loc) ->
+      virtual_method val_env meths self_type lab priv sty loc;
+      (val_env, met_env, par_env, fields, concr_meths)
 
-  (* Final class implementation and interface *)
-  let cl_imp =
-    { cl_args = cl_imp.cl_args;
-      cl_field = cl_imp.cl_field;
-      cl_pub_meths = public_methods;
-      cl_meths = cl_imp.cl_meths;
-      cl_loc = cl_imp.cl_loc }
-  in
-  let cl_sig =
-    { cty_params = params;
-      cty_args = args;
-      cty_vars = vars;
-      cty_meths = meths;
-      cty_self = exp_self;
-      cty_concr = cl_sig.cty_concr;
-      cty_new = cl_sig.cty_new }        (* new is still monomorphic *)
-  in let new_env = Env.add_class id cl_sig env in
-
-  ((cl, id, cl_id, obj_id, cl_sig, cl_imp), new_env)
-
-let make_abbrev env
-  (cl, id, cl_id, obj_id, cl_sig, cl_imp)
-  =
-  (* Class type abbreviation *)
-  let cl_abbrev =
-    (* Make a fully generic copy *)
-    Subst.type_declaration Subst.identity
-      { type_params = cl_sig.cty_params;
-        type_arity = List.length cl_sig.cty_params;
-        type_kind = Type_abstract;
-        type_manifest = Some
-          (if cl.pcl_closed = Closed then
-            Ctype.newgenty (Tconstr(Path.Pident obj_id, cl_sig.cty_params,
-                                    ref Mnil))
-          else begin
-            Ctype.set_object_name cl_sig.cty_self cl_sig.cty_params obj_id;
-            cl_sig.cty_self
-          end) }
-  in let new_env = Env.add_type cl_id cl_abbrev env in
-
-  (* Object type abbreviation *)
-  Ctype.begin_def ();
-  let (obj_ty_params, obj_ty) =
-    Ctype.instance_parameterized_type cl_sig.cty_params cl_sig.cty_self
-  in
-  Ctype.close_object obj_ty;
-  Ctype.end_def ();
-  List.iter Ctype.generalize obj_ty_params;
-  if not (List.for_all Ctype.closed_schema obj_ty_params) then
-    raise(Error(cl.pcl_loc,
-                Non_generalizable(obj_id, obj_ty_params)));
-  begin match Ctype.closed_schema_verbose obj_ty with
-    None -> ()
-  | Some v ->
-      raise(Error(cl.pcl_loc,
-                  Non_closed(obj_id, obj_ty_params, obj_ty, v)))
-  end;
-  Ctype.generalize obj_ty;
-  let obj_abbrev =
-    (* Make a fully generic copy *)
-    Subst.type_declaration Subst.identity
-      { type_params = obj_ty_params;
-        type_arity = List.length obj_ty_params;
-        type_kind = Type_abstract;
-        type_manifest =
-          Some (Ctype.unroll_abbrev obj_id obj_ty_params obj_ty) }
-  in let new_env = Env.add_type obj_id obj_abbrev new_env in
-
-  ((id, cl_sig, cl_id, cl_abbrev, obj_id, obj_abbrev, cl_imp), new_env)
-
-let transl_classes env cl =
-  let info =
-    List.map
-      (function cl ->
-        (cl, Ident.create cl.pcl_name, Ident.create ("#" ^ cl.pcl_name)))
-    cl
-  in
-  Ctype.init_def (Ident.current_time());
-  Ctype.begin_def ();
-  let (info, temp_env) = iter make_stub env info in
-  let (info, _) = iter (transl_class temp_env) env info in
-  let (info, new_env) = iter (build_new_type temp_env) env info in
-  Ctype.end_def ();
-  List.iter (fun (_, _, _, _, cl_sig, _) -> generalize_class cl_sig) info;
-  let (info, new_env) = iter make_abbrev new_env info in
-  (info, new_env)
-
-
-                              (****************************)
-                              (*  Class type translation  *)
-                              (****************************)
-
-
-let make_stub env (cl, obj_id, cl_id) =
-  Ctype.begin_def ();
-
-  (* Create self (class type) *)
-  let self = Ctype.newobj (Ctype.newvar ()) in
-
-  (* Find concrete methods and marks methods *)
-  let concr_meths =
-    List.fold_left
-      (function meths ->
-         function
-           Pctf_inher (nm, _, loc) ->
-             let (_, anc) =
-               try
-                 Env.lookup_class nm env
-               with Not_found ->
-                 raise(Error(loc, Unbound_class nm))
+  | Pcf_meth (lab, priv, expr, loc)  ->
+      Ctype.raise_nongen_level ();
+      let (_, ty) =
+        Ctype.filter_self_method val_env lab priv meths self_type
+      in
+      let meth_type = Ctype.newvar () in
+      let (obj_ty, res_ty) = Ctype.filter_arrow val_env meth_type in
+      Ctype.unify val_env obj_ty self_type;
+      Ctype.unify val_env res_ty ty;
+      let texp = type_expect met_env expr meth_type in
+      Ctype.end_def ();
+      (val_env, met_env, par_env, Cf_meth (lab, texp)::fields,
+       Concr.add lab concr_meths)
+
+  | Pcf_cstr (sty, sty', loc) ->
+      type_constraint val_env sty sty' loc;
+      (val_env, met_env, par_env, fields, concr_meths)
+
+  | Pcf_let (rec_flag, sdefs, loc) ->
+      let (defs, val_env) =
+        try
+          Typecore.type_let val_env rec_flag sdefs
+        with Ctype.Unify [(ty, _)] ->
+          raise(Error(loc, Make_nongen_seltype ty))
+      in
+      let (vals, met_env, par_env) =
+        List.fold_right
+          (fun id (vals, met_env, par_env) ->
+             let expr =
+               Typecore.type_exp val_env
+                 {pexp_desc = Pexp_ident (Longident.Lident (Ident.name id));
+                  pexp_loc = Location.none}
+             in
+             let desc =
+               {val_type = expr.exp_type; val_kind = Val_ivar Immutable}
              in
-               begin match (Ctype.expand_head env anc.cty_self).desc with
-                 Tobject (ty, _) ->
-                   add_methods env self ty;
-                   Concr.union anc.cty_concr meths
-               | _ -> fatal_error "Typeclass.make_stub (type)"
-               end
-         | Pctf_val _ ->
-             meths
-         | Pctf_virt (lab, priv, _, _) ->
-             Ctype.filter_method env lab priv self;
-             meths
-         | Pctf_meth (lab, priv, _, _) ->
-             Ctype.filter_method env lab priv self;
-             Concr.add lab meths)
-      Concr.empty cl.pcty_field
+             let id' = Ident.create (Ident.name id) in
+             ((id', expr)
+              :: vals,
+              Env.add_value id' desc met_env,
+              Env.add_value id' desc par_env))
+          (let_bound_idents defs)
+          ([], met_env, par_env)
+      in
+      (val_env, met_env, par_env, Cf_let (rec_flag, defs, vals)::fields,
+       concr_meths)
+
+  | Pcf_init expr ->
+      Ctype.raise_nongen_level ();
+      let meth_type = Ctype.newvar () in
+      let (obj_ty, res_ty) = Ctype.filter_arrow val_env meth_type in
+      Ctype.unify val_env obj_ty self_type;
+      Ctype.unify val_env res_ty (Ctype.instance Predef.type_unit);
+      let texp = type_expect met_env expr meth_type in
+      Ctype.end_def ();
+      (val_env, met_env, par_env, Cf_init texp::fields, concr_meths)
+
+and class_structure val_env met_env (spat, str) =
+  (* Environment for substructures *)
+  let par_env = met_env in
+
+  (* Self binder *)
+  let (pat, meths, vars, val_env, meth_env, par_env) =
+    type_self_pattern val_env met_env par_env spat
   in
+  let self_type = pat.pat_type in
 
-  Ctype.end_def ();
-  Ctype.generalize self;
+  (* Check that the binder has a correct type, and introduce a dummy
+     method preventing self type from being closed. *)
+  begin try Ctype.filter_method val_env dummy_method Private self_type with
+    Ctype.Unify _ ->
+      raise(Error(pat.pat_loc, Pattern_type_clash self_type))
+  end;
 
-  (* Temporary object type *)
-  let temp_obj_params =
-    List.map (fun _ -> Ctype.newvar ()) (fst cl.pcty_param)
-  in
-  let temp_obj = Ctype.instance self in
-  let obj_temp_abbrev =
-    { type_params = temp_obj_params;
-      type_arity = List.length temp_obj_params;
-      type_kind = Type_abstract;
-      type_manifest = Some temp_obj }
-  in
-  let temp_env = Env.add_type obj_id obj_temp_abbrev env in
-  let abbrev =
-    Ctype.newty (Tconstr (Path.Pident obj_id, temp_obj_params, ref Mnil))
+  (* Class fields *)
+  let (_, _, _, fields, concr_meths) =
+    List.fold_left (class_field self_type meths vars)
+      (val_env, meth_env, par_env, [], Concr.empty)
+      str
   in
 
-  (* Temporary class type *)
-  let (temp_cl_params, temp_cl) =
-    if cl.pcty_closed = Closed then
-      (temp_obj_params,
-       Ctype.newty (Tconstr(Path.Pident obj_id, temp_obj_params, ref Mnil)))
-    else begin
-      let params = List.map (fun _ -> Ctype.newvar ()) (fst cl.pcty_param) in
-      let ty = Ctype.instance self in
-      Ctype.set_object_name ty params obj_id;
-      (params, ty)
-    end
-  in
-  let cl_temp_abbrev =
-    { type_params = temp_cl_params;
-      type_arity = List.length temp_cl_params;
-      type_kind = Type_abstract;
-      type_manifest = Some temp_cl }
-  in let temp_env = Env.add_type cl_id cl_temp_abbrev temp_env
-  in let cl_abbrev =
-    Ctype.newty (Tconstr (Path.Pident cl_id, temp_cl_params, ref Mnil))
-  in
+  {cl_field = List.rev fields;
+   cl_meths = Meths.map (function (id, ty) -> id) !meths},
 
-  (* Temporary class type *)
-  let cl_temp_sig =
-    { cty_params = [];
-      cty_args = []; cty_vars = Vars.empty; cty_meths = Meths.empty;
-      cty_self = self; cty_concr = concr_meths;
-      cty_new = None }
-  in
-  let (id, temp_env) = Env.enter_class cl.pcty_name cl_temp_sig temp_env in
-
-  ((cl, id, cl_id, obj_id, self, concr_meths, temp_cl,
-    temp_cl_params, cl_abbrev, temp_obj, temp_obj_params, abbrev),
-   temp_env)
+  {cty_self = self_type;
+   cty_vars = Vars.map (function (id, mut, ty) -> (mut, ty)) !vars;
+   cty_concr = concr_meths }
 
-let type_class_field env var_env self cl (vars_sig, meths_sig) =
-  function
-    Pctf_inher (cl_name, params, loc) ->
-      (* Find class type *)
-      let (path, cl_type) =
-        try
-          Env.lookup_class cl_name env
-        with Not_found ->
-          raise (Error (loc, Unbound_class cl_name))
+and class_expr val_env met_env scl =
+  match scl.pcl_desc with
+    Pcl_constr (lid, styl) ->
+      let (path, decl) =
+        try Env.lookup_class lid val_env with Not_found ->
+          raise(Error(scl.pcl_loc, Unbound_class lid))
       in
-      let (params', _, vars', meths', self') = Ctype.instance_class cl_type in
-
-      (* Unify parameters *)
-      if List.length params <> List.length params' then
-        raise(Error(loc, Parameter_arity_mismatch
-                    (path, List.length params', List.length params)));
+      if Path.same decl.cty_path unbound_class then
+        raise(Error(scl.pcl_loc, Unbound_class_2 lid));
+      let tyl = List.map (transl_simple_type val_env false) styl in
+      let (params, clty) =
+        Ctype.instance_class decl.cty_params decl.cty_type
+      in
+      if List.length params <> List.length styl then
+        raise(Error(scl.pcl_loc,
+                    Parameter_arity_mismatch (lid, List.length params,
+                                                   List.length styl)));
       List.iter2
         (fun sty ty ->
-           let ty' = Typetexp.transl_simple_type var_env false sty in
-           try Ctype.unify var_env ty' ty with Ctype.Unify trace ->
+           let ty' = transl_simple_type val_env false sty in
+           try Ctype.unify val_env ty' ty with Ctype.Unify trace ->
              raise(Error(sty.ptyp_loc, Parameter_mismatch trace)))
-        params params';
-
-      let vars_sig =
-        Vars.fold
-          (fun lab (mut, ty) v_sig ->
-             insert_value var_env lab Public mut ty loc v_sig)
-          vars' vars_sig
+        styl params;
+      let cl =        
+        {cl_desc = Tclass_ident path;
+         cl_loc = scl.pcl_loc;
+         cl_type = clty}
       in
-
-      let meths_sig =
-        Meths.fold
-          (fun lab ty m_sig ->
-             let ty' =
-               try Meths.find lab m_sig with Not_found ->
-               Ctype.filter_method var_env lab Private self
-             in
-             begin try Ctype.unify env ty ty' with Ctype.Unify trace ->
-               raise(Error(loc, Method_type_mismatch (lab, trace)))
-             end;
-             Meths.add lab ty m_sig)
-          meths' meths_sig
+      let (vals, meths, concrs) = extract_constraints clty in
+      {cl_desc = Tclass_constraint (cl, vals, meths, concrs);
+       cl_loc = scl.pcl_loc;
+       cl_type = clty}
+  | Pcl_structure cl_str ->
+      let (desc, ty) = class_structure val_env met_env cl_str in
+      {cl_desc = Tclass_structure desc;
+       cl_loc = scl.pcl_loc;
+       cl_type = Tcty_signature ty}
+  | Pcl_fun (spat, scl') ->
+      let (pat, pv, val_env, met_env) =
+        Typecore.type_class_arg_pattern val_env met_env spat
       in
-
-      (* Self type *)
-      let ty' = Ctype.expand_head var_env self' in
-      begin match ty'.desc with
-        Tobject (fi, _) ->
-          if ty' != Ctype.expand_head var_env self then begin
-            if not (Ctype.opened_object ty') then
-              begin try
-                Ctype.unify var_env self (Ctype.newobj (closed_scheme fi))
-              with Ctype.Unify _ ->
-                let lab = missing_method var_env ty' self in
-                raise(Error(loc, Closed_ancestor (cl.pcty_name, path, lab)))
-              end;
-            Ctype.unify var_env ty' self;
-            type_meth var_env loc self fi
-          end
-      | _ ->
-          fatal_error "Typeclass.type_class_field (type)"
-      end;
-
-      (vars_sig, meths_sig)
-
-  | Pctf_val (lab, priv, mut, sty, loc) ->
-      begin match sty with
-        Some sty ->
-          let ty = transl_simple_type var_env false sty in
-          (insert_value var_env lab priv mut ty loc vars_sig, meths_sig)
-      | None ->
-          (fst (change_value_status lab priv mut loc vars_sig), meths_sig)
-      end
-
-  | Pctf_virt (lab, priv, sty, loc) ->
-      let ty = transl_simple_type var_env false sty in
-      let ty'' = Ctype.filter_method var_env lab priv self in
-      let ty' = try Meths.find lab meths_sig with Not_found -> ty'' in
-      begin try Ctype.unify var_env ty ty' with Ctype.Unify trace ->
-        raise(Error(loc, Method_type_mismatch (lab, trace)))
+      let pv =
+        List.map
+          (function (id, id', ty) ->
+            (id,
+             Typecore.type_exp val_env
+               {pexp_desc = Pexp_ident (Longident.Lident (Ident.name id));
+                pexp_loc = Location.none}))
+          pv
+      in
+      Parmatch.check_partial pat.pat_loc
+        [pat, (* Dummy expression *)
+              {exp_desc = Texp_constant (Asttypes.Const_int 1);
+               exp_loc = Location.none;
+               exp_type = Ctype.none;
+               exp_env = Env.empty }];
+      Ctype.raise_nongen_level ();
+      let cl = class_expr val_env met_env scl' in
+      Ctype.end_def ();
+      {cl_desc = Tclass_fun (pat, pv, cl);
+       cl_loc = scl.pcl_loc;
+       cl_type = Tcty_fun (pat.pat_type, cl.cl_type)}
+  | Pcl_apply (scl', sargs) ->
+      let cl = class_expr val_env met_env scl' in
+      let rec type_args ty_fun =
+        function
+          [] ->
+            ([], ty_fun)
+        | sarg1 :: sargl ->
+            begin match ty_fun with
+              Tcty_fun (ty, cty) ->
+                let arg1 = type_expect val_env sarg1 ty in
+                let (argl, ty_res) = type_args cty sargl in
+                (arg1 :: argl, ty_res)
+            | _ ->
+                raise(Error(cl.cl_loc, Cannot_apply cl.cl_type))
+            end
+      in
+      let (args, cty) = type_args cl.cl_type sargs in
+      begin try
+        make_nongen_class_type val_env cty
+      with Ctype.Unify [(ty, _)] ->
+        raise(Error(scl.pcl_loc, Make_nongen_seltype ty))
       end;
-      (vars_sig, Meths.add lab ty meths_sig)
-
-  | Pctf_meth (lab, priv, sty, loc) ->
-      let ty = transl_simple_type var_env false sty in
-      let ty'' = Ctype.filter_method var_env lab priv self in
-      let ty' = try Meths.find lab meths_sig with Not_found -> ty'' in
-      begin try Ctype.unify var_env ty ty' with Ctype.Unify trace ->
-        raise(Error(loc, Method_type_mismatch (lab, trace)))
+      {cl_desc = Tclass_apply (cl, args);
+       cl_loc = scl.pcl_loc;
+       cl_type = cty}
+  | Pcl_let (rec_flag, sdefs, scl') ->
+      let (defs, val_env) =
+        try
+          Typecore.type_let val_env rec_flag sdefs
+        with Ctype.Unify [(ty, _)] ->
+          raise(Error(scl.pcl_loc, Make_nongen_seltype ty))
+      in
+      let (vals, met_env) =
+        List.fold_right
+          (fun id (vals, met_env) ->
+             let expr =
+               Typecore.type_exp val_env
+                 {pexp_desc = Pexp_ident (Longident.Lident (Ident.name id));
+                  pexp_loc = Location.none}
+             in
+             let desc =
+               {val_type = expr.exp_type; val_kind = Val_ivar Immutable}
+             in
+             let id' = Ident.create (Ident.name id) in
+             ((id', expr)
+              :: vals,
+              Env.add_value id' desc met_env))
+          (let_bound_idents defs)
+          ([], met_env)
+      in
+      let cl = class_expr val_env met_env scl' in
+      {cl_desc = Tclass_let (rec_flag, defs, vals, cl);
+       cl_loc = scl.pcl_loc;
+       cl_type = cl.cl_type}
+  | Pcl_constraint (scl', scty) ->
+      Ctype.begin_class_def ();
+      Typetexp.narrow ();
+      let cl = class_expr val_env met_env scl' in
+      Typetexp.widen ();
+      Typetexp.narrow ();
+      let clty = class_type val_env scty in
+      Typetexp.widen ();
+      Ctype.end_def ();
+      generalize_class_type cl.cl_type;
+      generalize_class_type clty;
+      begin match Includeclass.class_types val_env cl.cl_type clty with
+        []    -> ()
+      | error -> raise(Error(cl.cl_loc, Class_match_failure error))
       end;
-      (vars_sig, Meths.add lab ty meths_sig)
+      let (vals, meths, concrs) = extract_constraints clty in
+      {cl_desc = Tclass_constraint (cl, vals, meths, concrs);
+       cl_loc = scl.pcl_loc;
+       cl_type = snd (Ctype.instance_class [] clty)}
+
+(*******************************)
+
+let temp_abbrev env id arity =
+  let params = ref [] in
+  for i = 1 to arity do
+    params := Ctype.newvar () :: !params
+  done;
+  let ty = Ctype.newobj (Ctype.newvar ()) in
+  let env =
+    Env.add_type id
+      {type_params = !params;
+       type_arity = arity;
+       type_kind = Type_abstract;
+       type_manifest = Some ty }
+      env
+  in
+  (!params, ty, env)
+
+let rec initial_env define_class (res, env) (cl, id, ty_id, obj_id, cl_id) =
+  (* Temporary abbreviations *)
+  let arity = List.length (fst cl.pci_params) in
+  let (obj_params, obj_ty, env) = temp_abbrev env obj_id arity in
+  let (cl_params, cl_ty, env) = temp_abbrev env cl_id arity in
+  
+  (* Temporary type for the class constructor *)
+  let constr_type = Ctype.newvar () in
+  let env =
+    let dummy_cty =
+      Tcty_signature
+        { cty_self = Ctype.newvar ();
+          cty_vars = Vars.empty;
+          cty_concr = Concr.empty }
+    in
+    Env.add_cltype ty_id
+      {clty_params = [];            (* Dummy value *)
+       clty_type = dummy_cty;       (* Dummy value *)
+       clty_path = unbound_class} (
+    if define_class then
+      Env.add_class id
+        {cty_params = [];             (* Dummy value *)
+         cty_type = dummy_cty;        (* Dummy value *)
+         cty_path = unbound_class;
+         cty_new =
+           match cl.pci_virt with
+             Virtual  -> None
+           | Concrete -> Some constr_type}
+        env
+    else
+      env)
+  in
+  ((cl, id, ty_id,
+    obj_id, obj_params, obj_ty,
+    cl_id, cl_params, cl_ty,
+    constr_type)::res,
+   env)
+
+let class_infos define_class kind
+    (cl, id, ty_id,
+     obj_id, obj_params, obj_ty,
+     cl_id, cl_params, cl_ty,
+     constr_type)
+    (res, env) =
 
-let transl_class temp_env env
-  (cl, id, cl_id, obj_id, self, concr_meths, temp_cl,
-   temp_cl_params, cl_abbrev, temp_obj, temp_obj_params, abbrev)
-    =
   reset_type_variables ();
-  Ctype.begin_def ();
-
-  (* Self type *)
-  let self = Ctype.instance self in
-
-  (* Introduce parameters *)
+  Ctype.begin_class_def ();
+  
+  (* Introduce class parameters *)
   let params =
     try
-      List.map (enter_type_variable true) (fst cl.pcty_param)
+      List.map (enter_type_variable true) (fst cl.pci_params)
     with Already_bound ->
-      raise(Error(snd cl.pcty_param, Repeated_parameter))
+      raise(Error(snd cl.pci_params, Repeated_parameter))
   in
-
-  (* Translate constrained parameters *)
-  let cstr_params =
-    List.map (function (v, _, loc) -> type_variable loc v) cl.pcty_cstr
+  
+  (* Type the class expression *)
+  let (expr, typ) = kind env cl.pci_expr in
+  
+  Ctype.end_def ();
+  
+  let sty = Ctype.self_type typ in
+
+  (* Generalize the row variable *)
+  let rv = Ctype.row_variable sty in
+  let rec limited_generalize rv =
+    function
+      Tcty_constr (path, params, cty) ->
+        List.iter (Ctype.limited_generalize rv) params;
+        limited_generalize rv cty
+    | Tcty_signature sign ->
+        Ctype.limited_generalize rv sign.cty_self;
+        Vars.iter (fun _ (_, ty) -> Ctype.limited_generalize rv ty)
+          sign.cty_vars
+    | Tcty_fun (ty, cty) ->
+        Ctype.limited_generalize rv ty;
+        limited_generalize rv cty
   in
-
-  (* Bind self type variable *)
-  begin match cl.pcty_self with
-      Some v -> Ctype.unify temp_env self (enter_type_variable false v)
-    | None   -> ()
+  List.iter (Ctype.limited_generalize rv) params;
+  limited_generalize rv typ;
+
+  (* Check the abbreviation for the object type *)
+  let (obj_params', obj_type) = Ctype.instance_class params typ in
+  let constr = Ctype.newconstr (Path.Pident obj_id) obj_params in
+  begin
+    let ty = Ctype.self_type obj_type in
+    Ctype.hide_private_methods ty;
+    Ctype.close_object ty;
+    begin try
+      List.iter2 (Ctype.unify env) obj_params obj_params'
+    with Ctype.Unify _ ->
+      raise(Error(cl.pci_loc,
+            Bad_parameters (obj_id, constr,
+                            Ctype.newconstr (Path.Pident obj_id)
+                                            obj_params')))
+    end;
+    begin try
+      Ctype.unify env ty constr
+    with Ctype.Unify _ ->
+      raise(Error(cl.pci_loc,
+        Abbrev_type_clash (constr, ty, Ctype.expand_head env constr)))
+    end
   end;
-
-  (* Add constraints *)
-  List.iter2
-    (fun (v, sty, loc) ty' ->
-       try
-         Ctype.unify temp_env (transl_simple_type temp_env false sty) ty'
-       with Ctype.Unify _ ->
-         raise(Error(loc, Unconsistent_constraint)))
-    cl.pcty_cstr cstr_params;
-
-  (* Translate argument types *)
-  let arg_sig = List.map (transl_simple_type temp_env false) cl.pcty_args in
-
-  (* Translate fields *)
-  let (vars_sig, meths_sig) =
-    List.fold_left (type_class_field env temp_env self cl)
-      (Vars.empty, Meths.empty) cl.pcty_field
-  in
-
-  (* Closeness of self *)
-  if cl.pcty_closed = Closed then
-    Ctype.close_object self;
-
-  (* Generalize class *)
-  Ctype.end_def ();
-  List.iter Ctype.generalize params;
-  List.iter Ctype.generalize arg_sig;
-  Vars.iter (fun l (m, t) -> Ctype.generalize t) vars_sig;
-  Meths.iter (fun l t -> Ctype.generalize t) meths_sig;
-  Ctype.generalize self;
-
-  (* Temporary class abbreviation *)
-  let (cl_params, cl_ty) = Ctype.instance_parameterized_type params self in
-  begin try Ctype.unify temp_env temp_cl cl_ty with Ctype.Unify _ ->
-    Ctype.remove_object_name temp_cl;
-    raise(Error(cl.pcty_loc, Abbrev_type_clash (cl_abbrev, cl_ty, temp_cl)))
+  
+  (* Check the other temporary abbreviation (#-type) *)
+  begin
+    let (cl_params', cl_type) = Ctype.instance_class params typ in
+    let ty = Ctype.self_type cl_type in
+    Ctype.hide_private_methods ty;
+    Ctype.set_object_name obj_id (Ctype.row_variable ty) cl_params ty;
+    begin try
+      List.iter2 (Ctype.unify env) cl_params cl_params'
+    with Ctype.Unify _ ->
+      raise(Error(cl.pci_loc,
+            Bad_parameters (cl_id,
+                            Ctype.newconstr (Path.Pident cl_id)
+                                            cl_params,
+                            Ctype.newconstr (Path.Pident cl_id)
+                                            cl_params')))
+    end;
+    begin try
+      Ctype.unify env ty cl_ty
+    with Ctype.Unify _ ->
+      let constr = Ctype.newconstr (Path.Pident cl_id) params in
+      raise(Error(cl.pci_loc, Abbrev_type_clash (constr, ty, cl_ty)))
+    end
   end;
+  
+  (* Type of the class constructor *)
   begin try
-    List.iter2 (Ctype.unify temp_env) temp_cl_params cl_params
-  with Ctype.Unify _ ->
-    raise(Error(cl.pcty_loc,
-          Bad_parameters (cl_id, cl_abbrev,
-                          Ctype.newty (Tconstr (Path.Pident cl_id, cl_params,
-                                                ref Mnil)))))
+    Ctype.unify env (constructor_type constr obj_type) constr_type
+  with Ctype.Unify trace ->
+    raise(Error(cl.pci_loc,
+                Constructor_type_mismatch (cl.pci_name, trace)))
   end;
 
-  (* Object abbreviation and arguments for new *)
-  let (obj_params, arg_sig', obj_ty) =
-    Ctype.instance_parameterized_type_2 params arg_sig self
+  (* Class and class type temporary definitions *)
+  let cltydef =
+    {clty_params = params; clty_type = class_body typ;
+     clty_path = Path.Pident obj_id}
+  and clty =
+    {cty_params = params; cty_type = typ;
+     cty_path = Path.Pident obj_id;
+     cty_new =
+       match cl.pci_virt with
+         Virtual  -> None
+       | Concrete -> Some constr_type}
   in
-  begin try Ctype.unify temp_env abbrev obj_ty with Ctype.Unify _ ->
-    raise(Error(cl.pcty_loc, Abbrev_type_clash (abbrev, obj_ty, temp_obj)))
-  end;
-  begin try
-    List.iter2 (Ctype.unify temp_env) temp_obj_params obj_params
-  with Ctype.Unify _ ->
-    raise(Error(cl.pcty_loc,
-          Bad_parameters (obj_id, abbrev,
-                          Ctype.newty (Tconstr (Path.Pident obj_id, obj_params,
-                                                ref Mnil)))))
+  let env =
+    Env.add_cltype ty_id cltydef (
+    if define_class then Env.add_class id clty env else env)
+  in
+
+  if cl.pci_virt = Concrete then begin
+    match virtual_methods typ with
+      []   -> ()
+    | mets -> raise(Error(cl.pci_loc, Virtual_class(define_class, mets)))
   end;
-  Ctype.close_object temp_obj;
-
-  (* Temporary class signature *)
-  let cl_sig =
-    { cty_params = params;
-      cty_args = arg_sig;
-      cty_vars = vars_sig;
-      cty_meths = meths_sig;
-      cty_self = self;
-      cty_concr = concr_meths;
-      cty_new = None }
+
+  (* Misc. *)
+  let arity = Ctype.class_type_arity typ in
+  let pub_meths =
+    let (fields, _) =
+      Ctype.flatten_fields (Ctype.object_fields (Ctype.expand_head env obj_ty))
+    in
+    List.map (function (lab, _, _) -> lab) fields
   in
-  let new_env = Env.add_class id cl_sig env in
-
-  ((cl, id, cl_id, obj_id, cl_sig, abbrev, temp_obj,
-    temp_obj_params),
-   new_env)
-
-let build_new_type temp_env env
-  (cl, id, cl_id, obj_id, cl_sig, abbrev, temp_obj,
-   temp_obj_params)
-    =
-  (* Modify constrainsts to ensure the object abbreviation is well-formed *)
-  let (params, args, vars, meths, self) = Ctype.instance_class cl_sig in
-  List.iter2 (Ctype.unify temp_env) params temp_obj_params;
-                                        (* Never fails *)
-
-  (* Hide private methods *)
-  Ctype.hide_private_methods cl_sig.cty_self;
-
-  (* Closeness of self (2) *)
-  if (cl.pcty_closed <> Closed) & not (Ctype.opened_object self) then
-    raise(Error(cl.pcty_loc, Closed_class cl.pcty_name));
-
-  equalize_methods temp_env self temp_obj;
-
-  (* self should not be an abbreviation (printtyp) *)
-  let exp_self = Ctype.expand_head temp_env self in
-
-  let new_ty =
-    if cl.pcty_kind = Concrete then
-      Some (List.fold_right
-              (fun arg ty -> Ctype.newty (Tarrow(arg, ty)))
-              args abbrev)
-    else
-      None
+  
+  (* Final definitions *)
+  let (params', typ') = Ctype.instance_class params typ in
+  let cltydef =
+    {clty_params = params'; clty_type = class_body typ';
+     clty_path = Path.Pident obj_id}
+  and clty =
+    {cty_params = params'; cty_type = typ';
+     cty_path = Path.Pident obj_id;
+     cty_new =
+       match cl.pci_virt with
+         Virtual  -> None
+       | Concrete -> Some constr_type}
   in
-
-  let public_methods =
-    match (Ctype.repr exp_self).desc with
-      Tobject (fi, _) ->
-        let (meths, _) = Ctype.flatten_fields fi in
-        List.map (function (lab, _, _) -> lab) meths
-    | _ -> fatal_error "Typeclass.build_new_type"
+  let obj_abbr =
+    {type_params = obj_params;
+     type_arity = List.length obj_params;
+     type_kind = Type_abstract;
+     type_manifest = Some obj_ty }
   in
+  let (cl_params, cl_ty) =
+    Ctype.instance_parameterized_type params (Ctype.self_type typ)
+  in
+  Ctype.hide_private_methods cl_ty;
+  Ctype.set_object_name obj_id (Ctype.row_variable cl_ty) cl_params cl_ty;
+  let cl_abbr =
+    {type_params = cl_params;
+     type_arity = List.length cl_params;
+     type_kind = Type_abstract;
+     type_manifest = Some cl_ty }
+  in
+  ((cl, id, clty, ty_id, cltydef, obj_id, obj_abbr, cl_id, cl_abbr,
+    arity, pub_meths, expr) :: res,
+   env)
+
+let final_env define_class
+    (cl, id, clty, ty_id, cltydef, obj_id, obj_abbr, cl_id, cl_abbr,
+     arity, pub_meths, expr)
+    (res, env) =
+
+  List.iter Ctype.generalize clty.cty_params;
+  generalize_class_type clty.cty_type;
+  begin match clty.cty_new with
+    None -> ()
+  | Some ty -> Ctype.generalize ty
+  end;
+  List.iter Ctype.generalize obj_abbr.type_params;
+  begin match obj_abbr.type_manifest with
+    None    -> ()
+  | Some ty -> Ctype.generalize ty
+  end;
+  List.iter Ctype.generalize cl_abbr.type_params;
+  begin match cl_abbr.type_manifest with
+    None    -> ()
+  | Some ty -> Ctype.generalize ty
+  end;
 
-  (* Check whether the class can be concrete *)
-  if cl.pcty_kind = Concrete then begin
-    List.iter
-      (function m ->
-         if not (Concr.mem m cl_sig.cty_concr) then
-           raise(Error(cl.pcty_loc, Virtual_class (cl.pcty_name, m))))
-      public_methods;
-    Meths.iter
-      (fun m _ ->
-         if not (Concr.mem m cl_sig.cty_concr) then
-           raise(Error(cl.pcty_loc, Virtual_class (cl.pcty_name, m))))
-      meths
+  begin match
+    Ctype.closed_class clty.cty_params
+      (Ctype.signature_of_class_type clty.cty_type)
+  with
+    None        -> ()
+  | Some reason ->
+      let printer =
+        if define_class then fun () -> Printtyp.class_declaration id clty
+        else fun () -> Printtyp.cltype_declaration id cltydef
+      in
+      raise(Error(cl.pci_loc, Unbound_type_var(printer, reason)))
   end;
 
-  (* Final class type *)
-  let cl_sig =
-    { cty_params = params;
-      cty_args = args;
-      cty_vars = vars;
-      cty_meths = meths;
-      cty_self = exp_self;
-      cty_concr = cl_sig.cty_concr;
-      cty_new = new_ty }
-  in let new_env = Env.add_class id cl_sig env in
-
-  ((cl, id, cl_id, obj_id, cl_sig), new_env)
-
-let make_abbrev env
-  (cl, id, cl_id, obj_id, cl_sig)
-    =
-  (* Class type abbreviation *)
-  let cl_abbrev =
-    { type_params = cl_sig.cty_params;
-      type_arity = List.length cl_sig.cty_params;
-      type_kind = Type_abstract;
-      type_manifest = Some
-        (if cl.pcty_closed = Closed then
-          Ctype.newgenty (Tconstr(Path.Pident obj_id, cl_sig.cty_params,
-                                  ref Mnil))
-        else begin
-          Ctype.set_object_name cl_sig.cty_self cl_sig.cty_params obj_id;
-          cl_sig.cty_self
-        end) }
-  in let new_env = Env.add_type cl_id cl_abbrev env in
-
-  (* Object type abbreviation *)
-  Ctype.begin_def ();
-  let (obj_ty_params, obj_ty) =
-    Ctype.instance_parameterized_type cl_sig.cty_params cl_sig.cty_self
+  let env =
+    Env.add_type obj_id obj_abbr (
+    Env.add_type cl_id cl_abbr (
+    Env.add_cltype ty_id cltydef (
+    if define_class then Env.add_class id clty env else env)))
   in
-  Ctype.close_object obj_ty;
-  Ctype.end_def ();
-  List.iter Ctype.generalize obj_ty_params;
-  begin match Ctype.closed_schema_verbose obj_ty with
-    None -> ()
-  | Some v ->
-      raise(Error(cl.pcty_loc,
-                  Non_closed(obj_id, obj_ty_params, obj_ty, v)))
-  end;
-  Ctype.generalize obj_ty;
-  let obj_abbrev =
-    { type_params = obj_ty_params;
-      type_arity = List.length obj_ty_params;
-      type_kind = Type_abstract;
-      type_manifest = Some (Ctype.unroll_abbrev obj_id obj_ty_params obj_ty) }
-  in let new_env = Env.add_type obj_id obj_abbrev new_env in
-
-  ((id, cl_sig, cl_id, cl_abbrev, obj_id, obj_abbrev), new_env)
-
-let rec transl_class_types env cl =
-  let info =
+  ((id, clty, ty_id, cltydef, obj_id, obj_abbr, cl_id, cl_abbr,
+    arity, pub_meths, expr)::res,
+   env)
+
+(*******************************)
+
+let type_classes define_class kind env cls =
+  let cls =
     List.map
       (function cl ->
-         (cl, Ident.create cl.pcty_name, Ident.create ("#" ^ cl.pcty_name)))
-      cl
+         (cl,
+          Ident.create cl.pci_name, Ident.create cl.pci_name,
+          Ident.create cl.pci_name, Ident.create ("#" ^ cl.pci_name)))
+      cls
+  in
+  Ctype.init_def (Ident.current_time ());
+  Ctype.begin_class_def ();
+  let (res, env) =
+    List.fold_left (initial_env define_class) ([], env) cls
+  in
+  let (res, env) =
+    List.fold_right (class_infos define_class kind) res ([], env)
   in
-  Ctype.init_def(Ident.current_time());
-  Ctype.begin_def();
-  let (info, temp_env) = iter make_stub env info in
-  let (info, _) = iter (transl_class temp_env) env info in
-  let (info, new_env) = iter (build_new_type temp_env) env info in
   Ctype.end_def ();
-  List.iter (fun (_, _, _, _, cl_sig) -> generalize_class cl_sig) info;
-  let (info, new_env) = iter make_abbrev new_env info in
-  (info, new_env)
+  (* Make type abbreviations fully generic *)
+  let (res, env) =
+    List.fold_right (final_env define_class) res ([], env)
+  in
+(*
+  let env =
+    List.fold_right
+      (fun (_, _, _, _, obj_id, obj_abbr, cl_id, cl_abbr, _, _, _) env ->
+         Env.add_type obj_id
+           (Subst.type_declaration Subst.identity obj_abbr) (
+         Env.add_type cl_id
+           (Subst.type_declaration Subst.identity cl_abbr) env))
+      res env
+  in
+*)
+  (List.rev res, env)
 
+let class_declaration env sexpr =
+  let expr = class_expr env env sexpr in
+  (expr, expr.cl_type)
+
+let class_description env sexpr =
+  let expr = class_type env sexpr in
+  (expr, expr)
+
+let class_declarations env cls =
+  type_classes true class_declaration env cls
+
+let class_descriptions env cls =
+  type_classes true class_description env cls
+
+let class_type_declarations env cls =
+  let (decl, env) =
+    type_classes false class_description env cls
+  in
+  (List.map
+     (function
+          (_, _, ty_id, cltydef, obj_id, obj_abbr, cl_id, cl_abbr, _, _, _) ->
+        (ty_id, cltydef, obj_id, obj_abbr, cl_id, cl_abbr))
+     decl,
+   env)
+
+(*******************************)
 
 (* Error report *)
 
 open Format
 
 let report_error = function
-    Duplicate_method s ->
-      print_string "Two methods are named"; print_space ();
-      print_string s
-  | Duplicate_variable s ->
-      print_string "Two instance variables are named"; print_space ();
-      print_string s
-  | Duplicate_super_variable s ->
-      print_string "Two ancestors are named"; print_space ();
-      print_string s
   | Repeated_parameter ->
       print_string "A type parameter occurs several times"
-  | Virtual_class (cl, met) ->
-      print_string "The class"; print_space ();
-      print_string cl; print_space ();
-      print_string "should be virtual: its method"; print_space ();
-      print_string met; print_space ();
-      print_string "is undefined"
-  | Closed_class cl ->
-      print_string "The class"; print_space ();
-      print_string cl; print_space ();
-      print_string "is closed, but not marked closed"
-  | Closed_ancestor (cl, anc, met) ->
-      print_string "The class"; print_space ();
-      print_string cl; print_space ();
-      print_string "inherits from the closed class"; print_space ();
-      Printtyp.path anc; print_space ();
-      print_string "which has no method"; print_space ();
-      print_string met
-  | Non_generalizable (id, params) ->
-      open_box 0;
-      Printtyp.reset ();
-      List.iter Printtyp.mark_loops params;
-      print_string "The";
-      List.iter (fun w -> print_space (); print_string w)
-        ["type"; "parameters"; "of"; "this"; "class"; "contains";
-         "type"; "variables"; "that"; "cannot"; "be"; "generalized:"];
-      print_break 1 2;
-      Printtyp.type_scheme
-        {desc = Tconstr(Path.Pident id, params, ref Mnil); level = 0};
-      close_box ()
-  | Non_closed (id, args, typ, var) ->
-      open_box 0;
-      Printtyp.reset ();
-      List.iter Printtyp.mark_loops args;
-      Printtyp.mark_loops typ;
-      begin match var with
-        Ctype.Var v ->
-          print_string "The type variable"; print_space ();
-          Printtyp.type_expr v; print_space ();
-          print_string "is not bound in implicit type definition"
-      | _ ->
-          print_string "Unbound row variable in implicit type definition"
-      end;
-      print_break 1 2;
-      open_box 0;
-      Printtyp.type_expr
-        (Ctype.newty (Tconstr(Path.Pident id, args, ref Mnil)));
-      print_space (); print_string "="; print_space ();
-      Printtyp.type_expr typ;
-      close_box ();
-      close_box ();
-      print_space ();
-      print_string "It should be captured by a class type parameter"
-  | Mutable_var v ->
-      print_string "The variable"; print_space ();
-      print_string v; print_space ();
-      print_string "was mutable and is redefined as immutable"
-  | Undefined_var v ->
-      print_string "The variable"; print_space ();
-      print_string v; print_space ();
-      print_string "is undefined"
-  | Variable_type_mismatch (v, trace) ->
+  | Unconsistent_constraint trace ->
       Printtyp.unification_error trace
         (function () ->
-           print_string "The variable ";
-           print_string v; print_space ();
-           print_string "has type")
+           print_string "The class constraints are not consistent : type")
         (function () ->
-           print_string "but is expected to have type")
+           print_string "is not compatible with type")
   | Method_type_mismatch (m, trace) ->
       Printtyp.unification_error trace
         (function () ->
@@ -1191,18 +943,41 @@ let report_error = function
            print_string "has type")
         (function () ->
            print_string "but is expected to have type")
-  | Unconsistent_constraint ->
-      print_string "The class constraints are not consistent"
+  | Structure_expected clty ->
+      open_box 0;
+      print_string
+        "This class expression is not a class structure; it has type";
+      print_space();
+      Printtyp.class_type clty;
+      close_box()
+  | Cannot_apply clty ->
+      print_string
+        "This class expression is not a class function, it cannot be applied"
+  | Pattern_type_clash ty ->
+      (* XXX Trace *)
+      (* XXX Revoir message d'erreur *)
+      open_box 0;
+      print_string "This pattern cannot match self: \
+                    it only matches values of type";
+      print_space ();
+      Printtyp.type_expr ty;
+      close_box ()
   | Unbound_class cl ->
       print_string "Unbound class"; print_space ();
       Printtyp.longident cl
-  | Argument_type_mismatch trace ->
-      Printtyp.unification_error trace
-        (function () ->
-           print_string "This argument has type")
-        (function () ->
-           print_string "but is expected to have type")
+  | Unbound_class_2 cl ->
+      print_string "The class"; print_space ();
+      Printtyp.longident cl; print_space ();
+      print_string "is not yet completely defined"
+  | Unbound_class_type cl ->
+      print_string "Unbound class type"; print_space ();
+      Printtyp.longident cl
+  | Unbound_class_type_2 cl ->
+      print_string "The class type"; print_space ();
+      Printtyp.longident cl; print_space ();
+      print_string "is not yet completely defined"
   | Abbrev_type_clash (abbrev, actual, expected) ->
+      (* XXX Afficher une trace ? *)
       open_box 0;
       Printtyp.reset ();
       Printtyp.mark_loops abbrev; Printtyp.mark_loops actual;
@@ -1214,6 +989,42 @@ let report_error = function
       print_string "but is used with type"; print_space ();
       Printtyp.type_expr expected;
       close_box ()
+  | Constructor_type_mismatch (c, trace) ->
+      Printtyp.unification_error trace
+        (function () ->
+           print_string "The expression \"new ";
+           print_string c;
+           print_string "\" has type")
+        (function () ->
+           print_string "but is used with type")
+  | Virtual_class (cl, mets) ->
+      open_vbox 0;
+      if cl then
+        print_string "This class should be virtual"
+      else
+        print_string "This class type should be virtual";
+      print_space ();
+      open_box 2;
+      print_string "The following methods are undefined :";
+      List.iter
+        (function met ->
+          print_space (); print_string met)
+        mets;
+      close_box (); close_box()
+  | Parameter_arity_mismatch(lid, expected, provided) ->
+      open_box 0;
+      print_string "The class constructor "; Printtyp.longident lid;
+      print_space(); print_string "expects "; print_int expected;
+      print_string " type argument(s),"; print_space();
+      print_string "but is here applied to "; print_int provided;
+      print_string " type argument(s)";
+      close_box()
+  | Parameter_mismatch trace ->
+      Printtyp.unification_error trace
+        (function () ->
+           print_string "The type parameter")
+        (function () ->
+           print_string "does not meet its constraint: it should be")
   | Bad_parameters (id, params, cstrs) ->
       open_box 0;
       Printtyp.reset ();
@@ -1225,28 +1036,51 @@ let report_error = function
       print_string "wich are incompatible with constraints"; print_space ();
       Printtyp.type_expr cstrs; print_space ();
       close_box ()
-  | Illdefined_class s ->
-      print_string "The class "; print_string s;
-      print_string " is ill-defined"
-  | Parameter_mismatch trace ->
-      Printtyp.unification_error trace
-        (function () ->
-           print_string "The type parameter")
-        (function () ->
-           print_string "does not meet its constraint: it should be")
-  | Argument_arity_mismatch(p, expected, provided) ->
+  | Class_match_failure error ->
+      Includeclass.report_error error
+  | Unbound_val lab ->
+      print_string "Unbound instance variable "; print_string lab
+  | Unbound_type_var (printer, reason) ->
+      open_vbox 0;
       open_box 0;
-      print_string "The class "; Printtyp.path p;
-      print_space(); print_string "expects "; print_int expected;
-      print_string " argument(s),"; print_space();
-      print_string "but is here applied to "; print_int provided;
-      print_string " argument(s)";
-      close_box()
-  | Parameter_arity_mismatch(p, expected, provided) ->
+      print_string "Some type variables are unbound in this type:";
+      print_break 1 2;
+      printer ();
+      close_box ();
+      print_space ();
       open_box 0;
-      print_string "The class "; Printtyp.path p;
-      print_space(); print_string "expects "; print_int expected;
-      print_string " type parameter(s),"; print_space();
-      print_string "but is here applied to "; print_int provided;
-      print_string " type parameter(s)";
-      close_box()
+      begin match reason with
+        Ctype.CC_Method (ty0, lab, ty) ->
+    (* XXX Cas ou une row variable n'est pas liee... *)
+          Printtyp.reset ();
+          Printtyp.mark_loops ty; Printtyp.mark_loops ty0;
+          print_string "The method"; print_space ();
+          print_string lab; print_space ();
+          print_string "has type"; print_break 1 2;
+          Printtyp.type_expr ty; print_space ();
+          print_string "where"; print_space ();
+          Printtyp.type_expr ty0; print_space ();
+          print_string "is unbound"
+      | Ctype.CC_Value (ty0, lab, ty) ->
+          Printtyp.reset ();
+          Printtyp.mark_loops ty; Printtyp.mark_loops ty0;
+          print_string "The instance variable"; print_space ();
+          print_string lab; print_space ();
+          print_string "has type"; print_break 1 2;
+          Printtyp.type_expr ty; print_space ();
+          print_string "where"; print_space ();
+          Printtyp.type_expr ty0; print_space ();
+          print_string "is unbound"
+      end;
+      close_box ();
+      close_box ()
+  | Make_nongen_seltype ty ->
+      open_vbox 0;
+      open_box 0;
+      print_string "Self type should not occur in the non-generic type";
+      print_break 1 2;
+      Printtyp.type_scheme ty;
+      close_box ();
+      print_cut ();
+      print_string "It would escape the scope of its class";
+      close_box ()
diff --git a/typing/typeclass.mli b/typing/typeclass.mli
index 6dbc7dd208..8ef9dc2db9 100644
--- a/typing/typeclass.mli
+++ b/typing/typeclass.mli
@@ -15,40 +15,49 @@ open Asttypes
 open Types
 open Typedtree
 
-val transl_classes:
-  Env.t -> Parsetree.class_def list ->
-  (Ident.t * class_type * Ident.t * type_declaration *
-   Ident.t * type_declaration * class_def) list * Env.t
-val transl_class_types:
-  Env.t -> Parsetree.class_type list ->
-  (Ident.t * class_type * Ident.t * type_declaration *
-   Ident.t * type_declaration) list * Env.t
+val class_declarations:
+  Env.t -> Parsetree.class_declaration list ->
+  (Ident.t * class_declaration *
+   Ident.t * cltype_declaration *
+   Ident.t * type_declaration *
+   Ident.t * type_declaration *
+   int * string list * class_expr) list * Env.t
+
+val class_descriptions:
+  Env.t -> Parsetree.class_description list ->
+  (Ident.t * class_declaration *
+   Ident.t * cltype_declaration *
+   Ident.t * type_declaration *
+   Ident.t * type_declaration *
+   int * string list * class_type) list * Env.t
 
+val class_type_declarations:
+  Env.t -> Parsetree.class_description list ->
+  (Ident.t * cltype_declaration *
+   Ident.t * type_declaration *
+   Ident.t * type_declaration) list * Env.t
 
 type error =
-    Duplicate_method of string
-  | Duplicate_variable of string
-  | Duplicate_super_variable of string
-  | Repeated_parameter
-  | Virtual_class of string * string
-  | Closed_class of string
-  | Closed_ancestor of string * Path.t * string
-  | Non_generalizable of Ident.t * type_expr list
-  | Non_closed of Ident.t * type_expr list * type_expr *
-                  Ctype.closed_schema_result
-  | Mutable_var of string
-  | Undefined_var of string
-  | Variable_type_mismatch of string * (type_expr * type_expr) list
+    Unconsistent_constraint of (type_expr * type_expr) list
   | Method_type_mismatch of string * (type_expr * type_expr) list
-  | Unconsistent_constraint
+  | Structure_expected of class_type
+  | Cannot_apply of class_type
+  | Pattern_type_clash of type_expr
+  | Repeated_parameter
   | Unbound_class of Longident.t
-  | Argument_type_mismatch of (type_expr * type_expr) list
+  | Unbound_class_2 of Longident.t
+  | Unbound_class_type of Longident.t
+  | Unbound_class_type_2 of Longident.t
   | Abbrev_type_clash of type_expr * type_expr * type_expr
-  | Bad_parameters of Ident.t * type_expr * type_expr
-  | Illdefined_class of string
-  | Argument_arity_mismatch of Path.t * int * int
-  | Parameter_arity_mismatch of Path.t * int * int
+  | Constructor_type_mismatch of string * (type_expr * type_expr) list
+  | Virtual_class of bool * string list
+  | Parameter_arity_mismatch of Longident.t * int * int
   | Parameter_mismatch of (type_expr * type_expr) list
+  | Bad_parameters of Ident.t * type_expr * type_expr
+  | Class_match_failure of Ctype.class_match_failure list
+  | Unbound_val of string
+  | Unbound_type_var of (unit -> unit) * Ctype.closed_class_failure
+  | Make_nongen_seltype of type_expr
 
 exception Error of Location.t * error
 
diff --git a/typing/typecore.ml b/typing/typecore.ml
index c842150ce1..7fd640f9e1 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -37,7 +37,8 @@ type error =
   | Label_missing
   | Label_not_mutable of Longident.t
   | Bad_format of string
-  | Undefined_method_err of string
+  | Undefined_method of type_expr * string
+  | Undefined_inherited_method of string
   | Unbound_class of Longident.t
   | Virtual_class of Longident.t
   | Unbound_instance_variable of string
@@ -48,6 +49,7 @@ type error =
   | Coercion_failure of type_expr * type_expr * (type_expr * type_expr) list
   | Too_many_arguments
   | Scoping_let_module of string * type_expr
+  | Masked_instance_variable of Longident.t
 
 exception Error of Location.t * error
 
@@ -190,7 +192,7 @@ let add_pattern_variables env =
   pattern_variables := [];
   List.fold_right
     (fun (id, ty) env ->
-      Env.add_value id {val_type = ty; val_kind = Val_reg} env)
+       Env.add_value id {val_type = ty; val_kind = Val_reg} env)
     pv env
 
 let type_pattern env spat =
@@ -205,6 +207,39 @@ let type_pattern_list env spatl =
   let new_env = add_pattern_variables env in
   (patl, new_env)
 
+let type_class_arg_pattern val_env met_env spat =
+  pattern_variables := [];
+  let pat = type_pat val_env spat in
+  let (pv, met_env) =
+    List.fold_right
+      (fun (id, ty) (pv, env) ->
+         let id' = Ident.create (Ident.name id) in
+         ((id', id, ty)::pv,
+          Env.add_value id' {val_type = ty; val_kind = Val_ivar Immutable}
+            env))
+      !pattern_variables ([], met_env)
+  in
+  let val_env = add_pattern_variables val_env in
+  (pat, pv, val_env, met_env)
+
+let type_self_pattern val_env met_env par_env spat =
+  pattern_variables := [];
+  let pat = type_pat val_env spat in
+  let meths = ref Meths.empty in
+  let vars = ref Vars.empty in
+  let pv = !pattern_variables in
+  pattern_variables := [];
+  let (val_env, met_env, par_env) =
+    List.fold_right
+      (fun (id, ty) (val_env, met_env, par_env) ->
+         (Env.add_value id {val_type = ty; val_kind = Val_unbound} val_env,
+          Env.add_value id {val_type = ty; val_kind = Val_self (meths, vars)}
+            met_env,
+          Env.add_value id {val_type = ty; val_kind = Val_unbound} par_env))
+      pv (val_env, met_env, par_env)
+  in
+  (pat, meths, vars, val_env, met_env, par_env)
+
 let rec iter_pattern f p =
   f p;
   match p.pat_desc with
@@ -307,12 +342,19 @@ let rec type_exp env sexp =
       begin try
         let (path, desc) = Env.lookup_value lid env in
         { exp_desc =
-            begin match (desc.val_kind, lid) with
-              (Val_ivar _, Longident.Lident lab) ->
-                let (path_self, _) =
+            begin match desc.val_kind with
+              Val_ivar _ ->
+                let (self_path, _) =
+                  Env.lookup_value (Longident.Lident "*self*") env
+                in
+                Texp_instvar(self_path, path)
+            | Val_self _ ->
+                let (path, _) =
                   Env.lookup_value (Longident.Lident "*self*") env
                 in
-                Texp_instvar (path_self, path)
+                Texp_ident(path, desc)
+            | Val_unbound ->
+                raise(Error(sexp.pexp_loc, Masked_instance_variable lid))
             | _ ->
                 Texp_ident(path, desc)
             end;
@@ -570,62 +612,70 @@ let rec type_exp env sexp =
         exp_type = body.exp_type;
         exp_env = env }
   | Pexp_send (e, met) ->
-      let object = type_exp env e in
+      let obj = type_exp env e in
       begin try
         let (exp, typ) =
-          match object.exp_desc with
-            Texp_ident(path, {val_kind = Val_self meths}) ->
-              begin try                 (* Private method *)
-                let (id, typ) = Meths.find met !meths in
-                (Texp_send(object, Tmeth_val id), typ)
-              with Not_found ->         (* Implicitely defined method *)
-                let id = Ident.create met in
-                let typ = filter_method env met Private object.exp_type in
-                meths := Meths.add met (id, typ) !meths;
-                (Texp_send(object, Tmeth_val id), typ)
-              end
+          match obj.exp_desc with
+            Texp_ident(path, {val_kind = Val_self (meths, _)}) ->
+              let (id, typ) =
+                filter_self_method env met Private meths obj.exp_type
+              in
+              (Texp_send(obj, Tmeth_val id), typ)
           | Texp_ident(path, {val_kind = Val_anc methods}) ->
-              let typ = filter_method env met Public object.exp_type in
-              let (path, desc) =
-                Env.lookup_value (Longident.Lident "*self*") env
+              let method_id =
+                begin try List.assoc met methods with Not_found ->
+                  raise(Error(e.pexp_loc, Undefined_inherited_method met))
+                end
               in
-              let method_id = List.assoc met methods in
-              let method_type = newvar () in
-              let (obj_ty, res_ty) = filter_arrow env method_type in
-              unify env obj_ty desc.val_type;
-              unify env res_ty typ;
-              (Texp_apply({exp_desc = Texp_ident(Path.Pident method_id,
-                                                 {val_type = method_type;
-                                                  val_kind = Val_reg});
-                           exp_loc = sexp.pexp_loc;
-                           exp_type = method_type;
-                           exp_env = env },
-                          [{exp_desc = Texp_ident(path, desc);
-                            exp_loc = object.exp_loc;
-                            exp_type = desc.val_type;
-                            exp_env = env }]),
-               typ)
+              begin match
+                Env.lookup_value (Longident.Lident "*self_pat*") env,
+                Env.lookup_value (Longident.Lident "*self*") env
+              with
+                (_, ({val_kind = Val_self (meths, _)} as desc)),
+                (path, _) ->
+                  let (_, typ) =
+                    filter_self_method env met Private meths obj.exp_type
+                  in
+                  let method_type = newvar () in
+                  let (obj_ty, res_ty) = filter_arrow env method_type in
+                  unify env obj_ty desc.val_type;
+                  unify env res_ty typ;
+                  (Texp_apply({exp_desc = Texp_ident(Path.Pident method_id,
+                                                     {val_type = method_type;
+                                                       val_kind = Val_reg});
+                                exp_loc = sexp.pexp_loc;
+                                exp_type = method_type;
+                                exp_env = env },
+                              [{exp_desc = Texp_ident(path, desc);
+                                 exp_loc = obj.exp_loc;
+                                 exp_type = desc.val_type;
+                                 exp_env = env }]),
+                   typ)
+              |  _ ->
+                  assert false
+              end
           | _ ->
-              (Texp_send(object, Tmeth_name met),
-               filter_method env met Public object.exp_type)
+              (Texp_send(obj, Tmeth_name met),
+               filter_method env met Public obj.exp_type)
         in
           { exp_desc = exp;
             exp_loc = sexp.pexp_loc;
             exp_type = typ;
             exp_env = env }
       with Unify _ ->
-        raise(Error(e.pexp_loc, Undefined_method_err met))
+        raise(Error(e.pexp_loc, Undefined_method (obj.exp_type, met)))
       end
   | Pexp_new cl ->
-      let (cl_path, cl_typ) =
+      let (cl_path, cl_decl) =
         try Env.lookup_class cl env with Not_found ->
           raise(Error(sexp.pexp_loc, Unbound_class cl))
       in
-        begin match cl_typ.cty_new with
+        begin match cl_decl.cty_new with
           None ->
             raise(Error(sexp.pexp_loc, Virtual_class cl))
         | Some ty ->
-            { exp_desc = Texp_new cl_path;
+            { exp_desc = Texp_new (cl_path,
+                                   Ctype.class_type_arity cl_decl.cty_type);
               exp_loc = sexp.pexp_loc;
               exp_type = instance ty;
               exp_env = env }
@@ -660,35 +710,37 @@ let rec type_exp env sexp =
            lab::l)
         lst
         [];
-      let (path_self, {val_type = self_ty}) =
+      begin match
         try
+          Env.lookup_value (Longident.Lident "*self_pat*") env,
           Env.lookup_value (Longident.Lident "*self*") env
         with Not_found ->
           raise(Error(sexp.pexp_loc, Outside_class))
-      in
-      let type_override (lab, snewval) =
-        begin try
-          let (path, desc) = Env.lookup_value (Longident.Lident lab) env in
-          match desc.val_kind with
-            Val_ivar _ ->
-              (path, type_expect env snewval desc.val_type)
-          | _ ->
-              raise(Error(sexp.pexp_loc, Unbound_instance_variable lab))
-        with
-          Not_found ->
-            raise(Error(sexp.pexp_loc, Unbound_instance_variable lab))
-        end
-      in
-      let modifs = List.map type_override lst in
-      { exp_desc = Texp_override(path_self, modifs);
-        exp_loc = sexp.pexp_loc;
-        exp_type = self_ty;
-        exp_env = env }
-      (* let obj = Oo.copy self in obj.x <- e; obj *)
+      with
+        (_, {val_type = self_ty; val_kind = Val_self (_, vars)}),
+        (path_self, _) ->
+          let type_override (lab, snewval) =
+            begin try
+              let (id, _, ty) = Vars.find lab !vars in
+              (Path.Pident id, type_expect env snewval ty)
+            with
+              Not_found ->
+                raise(Error(sexp.pexp_loc, Unbound_instance_variable lab))
+            end
+          in
+          let modifs = List.map type_override lst in
+          { exp_desc = Texp_override(path_self, modifs);
+            exp_loc = sexp.pexp_loc;
+            exp_type = self_ty;
+            exp_env = env }
+      | _ ->
+          assert false
+      end
   | Pexp_letmodule(name, smodl, sbody) ->
       let ty = newvar() in
       let modl = !type_module env smodl in
       let (id, new_env) = Env.enter_module name modl.mod_type env in
+      Ctype.init_def(Ident.current_time());
       let body = type_exp new_env sbody in
       (* Unification of body.exp_type with the fresh variable ty
          fails if and only if the prefix condition is violated,
@@ -738,6 +790,26 @@ and type_expect env sexp ty_expected =
         exp_loc = sexp.pexp_loc;
         exp_type = exp2.exp_type;
         exp_env = env }
+  | Pexp_function caselist ->
+      let (ty_arg, ty_res) =
+        try filter_arrow env ty_expected with Unify _ ->
+          raise(Error(sexp.pexp_loc, Too_many_arguments))
+      in
+      let cases =
+        List.map
+          (fun (spat, sexp) ->
+             let (pat, ext_env) = type_pattern env spat in
+             unify_pat env pat ty_arg;
+             let exp = type_expect ext_env sexp ty_res in
+             (pat, exp))
+          caselist
+      in
+      Parmatch.check_unused cases;
+      Parmatch.check_partial sexp.pexp_loc cases;
+      { exp_desc = Texp_function cases;
+        exp_loc = sexp.pexp_loc;
+        exp_type = newty (Tarrow(ty_arg, ty_res));
+        exp_env = env }
   | _ ->
       let exp = type_exp env sexp in
       unify_exp env exp ty_expected;
@@ -810,65 +882,6 @@ let type_expression env sexp =
   else make_nongen exp.exp_type;
   exp
 
-(* Typing of methods *)
-
-let rec type_expect_fun env sexp ty_expected =
-  match sexp.pexp_desc with
-    Pexp_function caselist ->
-      let (ty_arg, ty_res) =
-        try filter_arrow env ty_expected with Unify _ ->
-          raise(Error(sexp.pexp_loc, Too_many_arguments))
-      in
-      let cases =
-        List.map
-          (fun (spat, sexp) ->
-             let (pat, ext_env) = type_pattern env spat in
-             unify_pat env pat ty_arg;
-             let exp = type_expect_fun ext_env sexp ty_res in
-             (pat, exp))
-          caselist
-      in
-      Parmatch.check_unused cases;
-      Parmatch.check_partial sexp.pexp_loc cases;
-      { exp_desc = Texp_function cases;
-        exp_loc = sexp.pexp_loc;
-        exp_type = newty (Tarrow(ty_arg, ty_res));
-        exp_env = env }
-  | _ ->
-      type_expect env sexp ty_expected
-
-let type_method env self self_name meths sexp ty_expected =
-  let meths = ref meths in
-  let (obj, env) =
-    Env.enter_value "*self*" {val_type = self; val_kind = Val_reg} env
-  in
-  let pattern =
-    { pat_desc = Tpat_var obj;
-      pat_loc = Location.none;
-      pat_type = self;
-      pat_env = env }
-  in
-  let (pattern, env) =
-    match self_name with
-      None      ->
-        (pattern, env)
-    | Some name ->
-        let (self_name, env) =
-          Env.enter_value name {val_type = self; val_kind = Val_self meths} env
-        in
-        ({ pat_desc = Tpat_alias (pattern, self_name);
-           pat_loc = Location.none;
-           pat_type = self;
-           pat_env = env },
-         env)
-  in
-  let exp = type_expect_fun env sexp ty_expected in
-  { exp_desc = Texp_function [(pattern, exp)];
-    exp_loc = sexp.pexp_loc;
-    exp_type = newty (Tarrow(pattern.pat_type, exp.exp_type));
-    exp_env = env },
-  !meths
-
 (* Error report *)
 
 open Format
@@ -930,7 +943,18 @@ let report_error = function
       print_string " is not mutable"
   | Bad_format s ->
       print_string "Bad format `"; print_string s; print_string "'"
-  | Undefined_method_err me ->
+  | Undefined_method (ty, me) ->
+      open_vbox 0;
+      open_box 0;
+      print_string "This expression has type";
+      print_break 1 2;
+      type_expr ty;
+      close_box ();
+      print_cut ();
+      print_string "It has no method ";
+      print_string me;
+      close_box ()
+  | Undefined_inherited_method me ->
       print_string "This expression has no method ";
       print_string me
   | Unbound_class cl ->
@@ -955,7 +979,7 @@ let report_error = function
       trace true (fun _ -> print_string "is not a subtype of type") tr1;
       trace false (fun _ -> print_string "is not compatible with type") tr2
   | Outside_class ->
-      print_string "Object duplication outside a class definition."
+      print_string "This object duplication occurs outside a class definition."
   | Value_multiply_overridden v ->
       print_string "The instance variable "; print_string v;
       print_string " is overridden several times"
@@ -978,3 +1002,7 @@ let report_error = function
       print_space(); type_expr ty; print_space();
       print_string "In this type, the locally bound module name ";
       print_string id; print_string " escapes its scope"
+  | Masked_instance_variable lid ->
+      print_string "The instance variable "; longident lid; print_space ();
+      print_string
+        "cannot be accessed from the definition of another instance variable"
diff --git a/typing/typecore.mli b/typing/typecore.mli
index d09f2cebfe..0a92ccd418 100644
--- a/typing/typecore.mli
+++ b/typing/typecore.mli
@@ -16,19 +16,28 @@
 open Asttypes
 open Types
 
+val is_nonexpansive: Typedtree.expression -> bool
+
 val type_binding:
         Env.t -> rec_flag ->
           (Parsetree.pattern * Parsetree.expression) list -> 
           (Typedtree.pattern * Typedtree.expression) list * Env.t
+val type_let:
+        Env.t -> rec_flag ->
+          (Parsetree.pattern * Parsetree.expression) list -> 
+          (Typedtree.pattern * Typedtree.expression) list * Env.t
 val type_expression:
         Env.t -> Parsetree.expression -> Typedtree.expression
-val type_method:
-        Env.t -> type_expr -> string option ->
-        (Ident.t * Types.type_expr) Meths.t ->
-        Parsetree.expression -> type_expr ->
-        Typedtree.expression * (Ident.t * Types.type_expr) Meths.t
-val type_pattern_list:
-        Env.t -> Parsetree.pattern list -> Typedtree.pattern list * Env.t
+val type_class_arg_pattern:
+        Env.t -> Env.t -> Parsetree.pattern ->
+        Typedtree.pattern * (Ident.t * Ident.t * type_expr) list *
+        Env.t * Env.t
+val type_self_pattern:
+        Env.t -> Env.t -> Env.t -> Parsetree.pattern ->
+        Typedtree.pattern *
+        (Ident.t * type_expr) Meths.t ref *
+        (Ident.t * Asttypes.mutable_flag * type_expr) Vars.t ref *
+        Env.t * Env.t * Env.t
 val type_expect:
         Env.t -> Parsetree.expression -> type_expr ->
         Typedtree.expression
@@ -50,7 +59,8 @@ type error =
   | Label_missing
   | Label_not_mutable of Longident.t
   | Bad_format of string
-  | Undefined_method_err of string
+  | Undefined_method of type_expr * string
+  | Undefined_inherited_method of string
   | Unbound_class of Longident.t
   | Virtual_class of Longident.t
   | Unbound_instance_variable of string
@@ -61,6 +71,7 @@ type error =
   | Coercion_failure of type_expr * type_expr * (type_expr * type_expr) list
   | Too_many_arguments
   | Scoping_let_module of string * type_expr
+  | Masked_instance_variable of Longident.t
 
 exception Error of Location.t * error
 
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index 944a58e76f..2a2a7b0665 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -29,6 +29,7 @@ type error =
   | Unconsistent_constraint
   | Type_clash of (type_expr * type_expr) list
   | Null_arity_external
+  | Unbound_type_var
 
 exception Error of Location.t * error
 
@@ -72,40 +73,29 @@ let transl_declaration env (name, sdecl) (id, decl) =
     raise(Error(sdecl.ptype_loc, Repeated_parameter))
   end;
 
-  let cstr_params =
-    List.map (function (v, _, loc) -> type_variable loc v) sdecl.ptype_cstrs
-  in
-  List.iter2
-    (fun (v, sty, loc) ty' ->
+  List.iter
+    (function (sty, sty', loc) ->
        try
-         Ctype.unify env (transl_simple_type env false sty) ty'
+         Ctype.unify env (transl_simple_type env false sty)
+                         (transl_simple_type env false sty')
        with Ctype.Unify _ ->
          raise(Error(loc, Unconsistent_constraint)))
-    sdecl.ptype_cstrs cstr_params;
+    sdecl.ptype_cstrs;
 
-  let decl' =
-    { type_params = decl.type_params;
-      type_arity = decl.type_arity;
-      type_kind =
-        Type_abstract;
-      type_manifest =
-        begin match (decl.type_manifest, sdecl.ptype_manifest) with
-          (None, None) -> None
-        | (Some ty, Some sty) ->
-            let ty' =
-              Ctype.unroll_abbrev id decl.type_params
-                (transl_simple_type env true sty)
-            in
-            if Ctype.cyclic_abbrev env id ty' then
-              raise(Error(sdecl.ptype_loc, Recursive_abbrev name));
-            begin try Ctype.unify env ty' ty with Ctype.Unify trace ->
-              raise(Error(sdecl.ptype_loc, Type_clash trace))
-            end;
-            Some ty
-        | _ ->
-            fatal_error "Typedecl.transl_declaration"
-        end } in
-  (id, decl')
+  begin match sdecl.ptype_manifest with
+    None ->
+      ()
+  | Some sty ->
+      let ty = transl_simple_type env true sty in
+      if Ctype.cyclic_abbrev env id ty then
+        raise(Error(sdecl.ptype_loc, Recursive_abbrev name));
+      begin try
+        Ctype.unify env ty (Ctype.newconstr (Path.Pident id) decl.type_params) 
+      with Ctype.Unify trace ->
+        raise(Error(sdecl.ptype_loc, Type_clash trace))
+      end
+  end;
+  (id, decl)
 
 (* Second pass: representation *)
 let transl_declaration2 env (name, sdecl) (id, decl) =
@@ -261,6 +251,13 @@ let transl_type_decl env name_sdecl_list =
       (fun (id, decl) env -> Env.add_type id decl env)
       decls env
   in
+  (* Check that all type variable are closed *)
+  List.iter2
+    (fun (_, sdecl) (id, decl) ->
+       match Ctype.closed_type_decl decl with
+         Some _ -> raise(Error(sdecl.ptype_loc, Unbound_type_var))
+       | None   -> ())
+    name_sdecl_list decls;
   (* Check re-exportation *)
   List.iter2 (check_abbrev newenv) name_sdecl_list decls;
   (* Done *)
@@ -299,10 +296,10 @@ let transl_with_constraint env sdecl =
     with Already_bound ->
       raise(Error(sdecl.ptype_loc, Repeated_parameter)) in
   List.iter
-    (function (v, ty, loc) ->
+    (function (ty, ty', loc) ->
        try
-         Ctype.unify env
-           (type_variable loc v) (transl_simple_type env false ty)
+         Ctype.unify env (transl_simple_type env false ty)
+                         (transl_simple_type env false ty')
        with Ctype.Unify _ ->
          raise(Error(loc, Unconsistent_constraint)))
     sdecl.ptype_cstrs;
@@ -353,3 +350,5 @@ let report_error = function
            print_string "but is here used with type")
   | Null_arity_external ->
       print_string "External identifiers must be functions"
+  | Unbound_type_var ->
+      print_string "A type variable is unbound in this type declaration";
diff --git a/typing/typedecl.mli b/typing/typedecl.mli
index d5d5737f9e..17c9d42b4b 100644
--- a/typing/typedecl.mli
+++ b/typing/typedecl.mli
@@ -37,6 +37,7 @@ type error =
   | Unconsistent_constraint
   | Type_clash of (type_expr * type_expr) list
   | Null_arity_external
+  | Unbound_type_var
 
 exception Error of Location.t * error
 
diff --git a/typing/typedtree.ml b/typing/typedtree.ml
index d7f6df65c5..595faab2a9 100644
--- a/typing/typedtree.ml
+++ b/typing/typedtree.ml
@@ -63,7 +63,7 @@ and expression_desc =
       Ident.t * expression * expression * direction_flag * expression
   | Texp_when of expression * expression
   | Texp_send of expression * meth
-  | Texp_new of Path.t
+  | Texp_new of Path.t * int
   | Texp_instvar of Path.t * Path.t
   | Texp_setinstvar of Path.t * Path.t * expression
   | Texp_override of Path.t * (Path.t * expression) list
@@ -73,21 +73,33 @@ and meth =
     Tmeth_name of string
   | Tmeth_val of Ident.t
 
-(* Value expressions for classes *)
+(* Value expressions for the class language *)
+
+and class_expr =
+  { cl_desc: class_expr_desc;
+    cl_loc: Location.t;
+    cl_type: class_type }
+
+and class_expr_desc =
+    Tclass_ident of Path.t
+  | Tclass_structure of class_structure
+  | Tclass_fun of pattern * (Ident.t * expression) list * class_expr
+  | Tclass_apply of class_expr * expression list
+  | Tclass_let of rec_flag *  (pattern * expression) list *
+                  (Ident.t * expression) list * class_expr
+  | Tclass_constraint of class_expr * string list * string list * Concr.t
+
+and class_structure =
+  { cl_field: class_field list;
+    cl_meths: Ident.t Meths.t }
 
 and class_field =
-    Cf_inher of
-      Path.t * expression list * (string * Ident.t) list *
-      (string * Ident.t) list * string list
-  | Cf_val of string * Ident.t * private_flag * expression option
+    Cf_inher of class_expr * (string * Ident.t) list * (string * Ident.t) list
+  | Cf_val of string * Ident.t * expression
   | Cf_meth of string * expression
-
-and class_def =
-  { cl_args: pattern list;
-    cl_field: class_field list;
-    cl_pub_meths: string list;
-    cl_meths: Ident.t Meths.t;
-    cl_loc: Location.t }
+  | Cf_let of rec_flag * (pattern * expression) list *
+              (Ident.t * expression) list
+  | Cf_init of expression
 
 (* Value expressions for the module language *)
 
@@ -115,7 +127,8 @@ and structure_item =
   | Tstr_module of Ident.t * module_expr
   | Tstr_modtype of Ident.t * module_type
   | Tstr_open of Path.t
-  | Tstr_class of (Ident.t * class_def) list
+  | Tstr_class of (Ident.t * int * string list * class_expr) list
+  | Tstr_cltype of (Ident.t * cltype_declaration) list
 
 and module_coercion =
     Tcoerce_none
diff --git a/typing/typedtree.mli b/typing/typedtree.mli
index 7daedd18f2..def8e0be87 100644
--- a/typing/typedtree.mli
+++ b/typing/typedtree.mli
@@ -62,7 +62,7 @@ and expression_desc =
       Ident.t * expression * expression * direction_flag * expression
   | Texp_when of expression * expression
   | Texp_send of expression * meth
-  | Texp_new of Path.t
+  | Texp_new of Path.t * int
   | Texp_instvar of Path.t * Path.t
   | Texp_setinstvar of Path.t * Path.t * expression
   | Texp_override of Path.t * (Path.t * expression) list
@@ -72,21 +72,35 @@ and meth =
     Tmeth_name of string
   | Tmeth_val of Ident.t
 
-(* Value expressions for classes *)
+(* Value expressions for the class language *)
+
+and class_expr =
+  { cl_desc: class_expr_desc;
+    cl_loc: Location.t;
+    cl_type: class_type }
+
+and class_expr_desc =
+    Tclass_ident of Path.t
+  | Tclass_structure of class_structure
+  | Tclass_fun of pattern * (Ident.t * expression) list * class_expr
+  | Tclass_apply of class_expr * expression list
+  | Tclass_let of rec_flag *  (pattern * expression) list *
+                  (Ident.t * expression) list * class_expr
+  | Tclass_constraint of class_expr * string list * string list * Concr.t
+    (* Visible instance variables, methods and concretes methods *)
+
+and class_structure =
+  { cl_field: class_field list;
+    cl_meths: Ident.t Meths.t }
 
 and class_field =
-    Cf_inher of
-      Path.t * expression list * (string * Ident.t) list *
-      (string * Ident.t) list * string list
-  | Cf_val of string * Ident.t * private_flag * expression option
+    Cf_inher of class_expr * (string * Ident.t) list * (string * Ident.t) list
+    (* Inherited instance variables and concrete methods *)
+  | Cf_val of string * Ident.t * expression
   | Cf_meth of string * expression
-
-and class_def =
-  { cl_args: pattern list;
-    cl_field: class_field list;
-    cl_pub_meths: string list;
-    cl_meths: Ident.t Meths.t;
-    cl_loc: Location.t }
+  | Cf_let of rec_flag * (pattern * expression) list *
+              (Ident.t * expression) list
+  | Cf_init of expression
 
 (* Value expressions for the module language *)
 
@@ -114,7 +128,8 @@ and structure_item =
   | Tstr_module of Ident.t * module_expr
   | Tstr_modtype of Ident.t * module_type
   | Tstr_open of Path.t
-  | Tstr_class of (Ident.t * class_def) list
+  | Tstr_class of (Ident.t * int * string list * class_expr) list
+  | Tstr_cltype of (Ident.t * cltype_declaration) list
 
 and module_coercion =
     Tcoerce_none
diff --git a/typing/typemod.ml b/typing/typemod.ml
index 67e06be009..6d3cea6e99 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -33,7 +33,7 @@ type error =
   | With_mismatch of Longident.t * Includemod.error list
   | Repeated_name of string * string
   | Non_generalizable of type_expr
-  | Non_generalizable_class of Ident.t * class_type
+  | Non_generalizable_class of Ident.t * class_declaration
   | Non_generalizable_module of module_type
 
 exception Error of Location.t * error
@@ -154,12 +154,21 @@ and transl_signature env sg =
       let rem = transl_signature newenv srem in
       sg @ rem
   | {psig_desc = Psig_class cl} :: srem ->
-      let (classes, newenv) = Typeclass.transl_class_types env cl in
+      let (classes, newenv) = Typeclass.class_descriptions env cl in
+      let rem = transl_signature newenv srem in
+      List.flatten
+        (map_end
+           (fun (i, d, i', d', i'', d'', i''', d''', _, _, _) ->
+              [Tsig_class(i, d);    Tsig_cltype(i', d');
+               Tsig_type(i'', d''); Tsig_type(i''', d''')])
+           classes [rem])
+  | {psig_desc = Psig_class_type cl} :: srem ->
+      let (classes, newenv) = Typeclass.class_type_declarations env cl in
       let rem = transl_signature newenv srem in
       List.flatten
         (map_end
            (fun (i, d, i', d', i'', d'') ->
-              [Tsig_class(i, d); Tsig_type(i', d'); Tsig_type(i'', d'')])
+              [Tsig_cltype(i, d); Tsig_type(i', d'); Tsig_type(i'', d'')])
            classes [rem])
 
 and transl_modtype_info env sinfo =
@@ -210,7 +219,12 @@ let check_unique_names sg =
     | Pstr_open lid -> ()
     | Pstr_class decl ->
         List.iter
-          (fun {pcl_name = name} ->
+          (fun {pci_name = name} ->
+             check "type" item.pstr_loc type_names name)
+          decl
+    | Pstr_class_type decl ->
+        List.iter
+          (fun {pci_name = name} ->
              check "type" item.pstr_loc type_names name)
           decl
   in
@@ -218,12 +232,6 @@ let check_unique_names sg =
 
 (* Check that all core type schemes in a structure are closed *)
 
-let closed_class classty =
-  List.for_all Ctype.closed_schema classty.cty_params &
-  List.for_all Ctype.closed_schema classty.cty_args &
-  Vars.fold (fun _ (_, ty) -> (or) (Ctype.closed_schema ty))
-            classty.cty_vars true
-
 let rec closed_modtype = function
     Tmty_ident p -> true
   | Tmty_signature sg -> List.for_all closed_signature_item sg
@@ -232,7 +240,6 @@ let rec closed_modtype = function
 and closed_signature_item = function
     Tsig_value(id, desc) -> Ctype.closed_schema desc.val_type
   | Tsig_module(id, mty) -> closed_modtype mty
-  | Tsig_class(id, classty) -> closed_class classty
   | _ -> true
 
 let check_nongen_scheme env = function
@@ -242,14 +249,6 @@ let check_nongen_scheme env = function
           if not (Ctype.closed_schema exp.exp_type) then
             raise(Error(exp.exp_loc, Non_generalizable exp.exp_type)))
         pat_exp_list
-  | Tstr_class cl ->
-      List.iter
-        (fun (id, imp) ->
-           let desc = Env.find_class (Pident id) env in
-           if not (closed_class desc) then
-             raise(Error(imp.cl_loc,
-                   Non_generalizable_class (id, desc))))
-        cl
   | Tstr_module(id, md) ->
       if not (closed_modtype md.mod_type) then
         raise(Error(md.mod_loc, Non_generalizable_module md.mod_type))
@@ -385,17 +384,40 @@ and type_struct env sstr =
       let (path, mty) = type_module_path env loc lid in
       let sg = extract_sig_open env loc mty in
       type_struct (Env.open_signature path sg env) srem
-  | {pstr_desc = Pstr_class cl; pstr_loc = loc} :: srem ->
-      let (classes, new_env) = Typeclass.transl_classes env cl in
+  | {pstr_desc = Pstr_class cl} :: srem ->
+      let (classes, new_env) = Typeclass.class_declarations env cl in
+      let (str_rem, sig_rem, final_env) = type_struct new_env srem in
+      (Tstr_class
+         (List.map (fun (i, _,_,_,_,_,_,_, s, m, c) ->
+            (i, s, m, c)) classes) ::
+       Tstr_cltype
+         (List.map (fun (_,_, i, d, _,_,_,_,_,_,_) -> (i, d)) classes) ::
+       Tstr_type
+         (List.map (fun (_,_,_,_, i, d, _,_,_,_,_) -> (i, d)) classes) ::
+       Tstr_type
+         (List.map (fun (_,_,_,_,_,_, i, d, _,_,_) -> (i, d)) classes) ::
+       str_rem,
+       List.flatten
+         (map_end
+            (fun (i, d, i', d', i'', d'', i''', d''', _, _, _) ->
+               [Tsig_class(i, d);    Tsig_cltype(i', d');
+                Tsig_type(i'', d''); Tsig_type(i''', d''')])
+            classes [sig_rem]),
+       final_env)
+  | {pstr_desc = Pstr_class_type cl} :: srem ->
+      let (classes, new_env) = Typeclass.class_type_declarations env cl in
       let (str_rem, sig_rem, final_env) = type_struct new_env srem in
-      (Tstr_class (List.map (fun (i, _, _, _, _, _, c) -> (i, c)) classes)
-       :: Tstr_type (List.map (fun (_, _, i, d, _, _, _) -> (i, d)) classes)
-       :: Tstr_type (List.map (fun (_, _, _, _, i, d, _) -> (i, d)) classes)
-       :: str_rem,
+      (Tstr_cltype
+         (List.map (fun (i, d, _, _, _, _) -> (i, d)) classes) ::
+       Tstr_type
+         (List.map (fun (_, _, i, d, _, _) -> (i, d)) classes) ::
+       Tstr_type
+         (List.map (fun (_, _, _, _, i, d) -> (i, d)) classes) ::
+       str_rem,
        List.flatten
          (map_end
-            (fun (i, d, i', d', i'', d'', _) ->
-               [Tsig_class(i, d); Tsig_type(i', d'); Tsig_type(i'', d'')])
+            (fun (i, d, i', d', i'', d'') ->
+               [Tsig_cltype(i, d); Tsig_type(i', d'); Tsig_type(i'', d'')])
             classes [sig_rem]),
        final_env)
 
@@ -489,7 +511,7 @@ let report_error = function
   | Non_generalizable_class (id, desc) ->
       open_box 0;
       print_string "The type of this class,"; print_space();
-      class_type id desc; print_string ","; print_space();
+      class_declaration id desc; print_string ","; print_space();
       print_string "contains type variables that cannot be generalized";
       close_box()
   | Non_generalizable_module mty ->
diff --git a/typing/typemod.mli b/typing/typemod.mli
index c5fad7d0b9..367fe209be 100644
--- a/typing/typemod.mli
+++ b/typing/typemod.mli
@@ -39,7 +39,7 @@ type error =
   | With_mismatch of Longident.t * Includemod.error list
   | Repeated_name of string * string
   | Non_generalizable of type_expr
-  | Non_generalizable_class of Ident.t * class_type
+  | Non_generalizable_class of Ident.t * class_declaration
   | Non_generalizable_module of module_type
 
 exception Error of Location.t * error
diff --git a/typing/types.ml b/typing/types.ml
index ab8dc46daf..d4ff8f58d0 100644
--- a/typing/types.ml
+++ b/typing/types.ml
@@ -34,7 +34,7 @@ and type_desc =
 
 and abbrev_memo =
     Mnil
-  | Mcons of Path.t * type_expr * abbrev_memo
+  | Mcons of Path.t * type_expr * type_expr * abbrev_memo
   | Mlink of abbrev_memo ref
 
 and field_kind =
@@ -42,10 +42,11 @@ and field_kind =
   | Fpresent
   | Fabsent
 
-(* A set of methods, with their types *)
+(* Maps of methods and instance variables *)
 
 module OrderedString = struct type t = string let compare = compare end
 module Meths = Map.Make(OrderedString)
+module Vars = Meths
 
 (* Value descriptions *)
 
@@ -57,9 +58,11 @@ and value_kind =
     Val_reg                             (* Regular value *)
   | Val_prim of Primitive.description   (* Primitive *)
   | Val_ivar of mutable_flag            (* Instance variable (mutable ?) *)
-  | Val_self of (Ident.t * type_expr) Meths.t ref
+  | Val_self of (Ident.t * type_expr) Meths.t ref *
+                (Ident.t * Asttypes.mutable_flag * type_expr) Vars.t ref
                                         (* Self *)
   | Val_anc of (string * Ident.t) list  (* Ancestor *)
+  | Val_unbound                         (* Unbound variable *)
 
 (* Constructor descriptions *)
 
@@ -90,20 +93,6 @@ and record_representation =
     Record_regular                      (* All fields are boxed / tagged *)
   | Record_float                        (* All fields are floats *)
 
-(* Type expressions for classes *)
-
-module Vars = Map.Make(OrderedString)
-module Concr = Set.Make(OrderedString)
-
-type class_type =
-  { cty_params: type_expr list;
-    cty_args: type_expr list;
-    cty_vars: (Asttypes.mutable_flag * type_expr) Vars.t;
-    cty_meths: type_expr Meths.t;
-    cty_self: type_expr;
-    cty_concr: Concr.t;
-    mutable cty_new: type_expr option }
-
 (* Type definitions *)
 
 type type_declaration =
@@ -119,6 +108,31 @@ and type_kind =
 
 type exception_declaration = type_expr list
 
+(* Type expressions for the class language *)
+
+module Concr = Set.Make(OrderedString)
+
+type class_type =
+    Tcty_constr of Path.t * type_expr list * class_type
+  | Tcty_signature of class_signature
+  | Tcty_fun of type_expr * class_type
+
+and class_signature =
+  { cty_self: type_expr;
+    cty_vars: (Asttypes.mutable_flag * type_expr) Vars.t;
+    cty_concr: Concr.t }
+
+type class_declaration =
+  { cty_params: type_expr list;
+    cty_type: class_type;
+    cty_path: Path.t;
+    cty_new: type_expr option }
+
+type cltype_declaration =
+  { clty_params: type_expr list;
+    clty_type: class_type;
+    clty_path: Path.t }
+
 (* Type expressions for the module language *)
 
 type module_type =
@@ -134,7 +148,8 @@ and signature_item =
   | Tsig_exception of Ident.t * exception_declaration
   | Tsig_module of Ident.t * module_type
   | Tsig_modtype of Ident.t * modtype_declaration
-  | Tsig_class of Ident.t * class_type
+  | Tsig_class of Ident.t * class_declaration
+  | Tsig_cltype of Ident.t * cltype_declaration
 
 and modtype_declaration =
     Tmodtype_abstract
diff --git a/typing/types.mli b/typing/types.mli
index ea0665d512..6e8cca99a8 100644
--- a/typing/types.mli
+++ b/typing/types.mli
@@ -33,7 +33,7 @@ and type_desc =
 
 and abbrev_memo =
     Mnil
-  | Mcons of Path.t * type_expr * abbrev_memo
+  | Mcons of Path.t * type_expr * type_expr * abbrev_memo
   | Mlink of abbrev_memo ref
 
 and field_kind =
@@ -41,9 +41,10 @@ and field_kind =
   | Fpresent
   | Fabsent
 
-(* A set of methods, with their types *)
+(* Maps of methods and instance variables *)
 
 module Meths : Map.S with type key = string
+module Vars  : Map.S with type key = string
 
 (* Value descriptions *)
 
@@ -55,9 +56,11 @@ and value_kind =
     Val_reg                             (* Regular value *)
   | Val_prim of Primitive.description   (* Primitive *)
   | Val_ivar of mutable_flag            (* Instance variable (mutable ?) *)
-  | Val_self of (Ident.t * type_expr) Meths.t ref
+  | Val_self of (Ident.t * type_expr) Meths.t ref *
+                (Ident.t * Asttypes.mutable_flag * type_expr) Vars.t ref
                                         (* Self *)
   | Val_anc of (string * Ident.t) list  (* Ancestor *)
+  | Val_unbound                         (* Unbound variable *)
 
 (* Constructor descriptions *)
 
@@ -88,20 +91,6 @@ and record_representation =
     Record_regular                      (* All fields are boxed / tagged *)
   | Record_float                        (* All fields are floats *)
 
-(* Type expressions for classes *)
-
-module Vars  : Map.S with type key = string
-module Concr : Set.S with type elt = string
-
-type class_type =
-  { cty_params: type_expr list;
-    cty_args: type_expr list;
-    cty_vars: (mutable_flag * type_expr) Vars.t;
-    cty_meths: type_expr Meths.t;
-    cty_self: type_expr;
-    cty_concr: Concr.t;
-    mutable cty_new: type_expr option }
-
 (* Type definitions *)
 
 type type_declaration =
@@ -117,6 +106,31 @@ and type_kind =
 
 type exception_declaration = type_expr list
 
+(* Type expressions for the class language *)
+
+module Concr : Set.S with type elt = string
+
+type class_type =
+    Tcty_constr of Path.t * type_expr list * class_type
+  | Tcty_signature of class_signature
+  | Tcty_fun of type_expr * class_type
+
+and class_signature =
+  { cty_self: type_expr;
+    cty_vars: (Asttypes.mutable_flag * type_expr) Vars.t;
+    cty_concr: Concr.t }
+
+type class_declaration =
+  { cty_params: type_expr list;
+    cty_type: class_type;
+    cty_path: Path.t;
+    cty_new: type_expr option }
+
+type cltype_declaration =
+  { clty_params: type_expr list;
+    clty_type: class_type;
+    clty_path: Path.t }
+
 (* Type expressions for the module language *)
 
 type module_type =
@@ -132,7 +146,8 @@ and signature_item =
   | Tsig_exception of Ident.t * exception_declaration
   | Tsig_module of Ident.t * module_type
   | Tsig_modtype of Ident.t * modtype_declaration
-  | Tsig_class of Ident.t * class_type
+  | Tsig_class of Ident.t * class_declaration
+  | Tsig_cltype of Ident.t * cltype_declaration
 
 and modtype_declaration =
     Tmodtype_abstract
diff --git a/typing/typetexp.ml b/typing/typetexp.ml
index 49af0d9462..2bef429ff7 100644
--- a/typing/typetexp.ml
+++ b/typing/typetexp.ml
@@ -37,6 +37,7 @@ exception Error of Location.t * error
 
 let type_variables = ref (Tbl.empty : (string, type_expr) Tbl.t)
 let aliases        = ref (Tbl.empty : (string, type_expr) Tbl.t)
+let saved_type_variables = ref ([] : (string, type_expr) Tbl.t list)
 
 let used_variables = ref (Tbl.empty : (string, type_expr) Tbl.t)
 let bindings       = ref ([] : (type_expr * type_expr) list)
@@ -44,7 +45,18 @@ let bindings       = ref ([] : (type_expr * type_expr) list)
 
 let reset_type_variables () =
   reset_global_level ();
-  type_variables := Tbl.empty
+  type_variables := Tbl.empty;
+  saved_type_variables := []
+
+let narrow () =
+  increase_global_level ();
+  saved_type_variables := !type_variables :: !saved_type_variables
+
+let widen () =
+  restore_global_level ();
+  match !saved_type_variables with
+    tv :: rem -> type_variables := tv; saved_type_variables := rem
+  | []        -> assert false
 
 let enter_type_variable strict name =
   try
@@ -116,8 +128,9 @@ let rec transl_type env policy styp =
         raise(Error(styp.ptyp_loc, Type_arity_mismatch(lid, decl.type_arity,
                                                            List.length stl)));
       let args = List.map (transl_type env policy) stl in
-      let cstr = newty (Tconstr(path, args, ref Mnil)) in
-      let params = Ctype.instance_list decl.type_params in
+      let params = List.map (fun _ -> Ctype.newvar ()) args in
+      let cstr = newty (Tconstr(path, params, ref Mnil)) in
+      Ctype.expand_head env cstr;
       List.iter2
         (fun (sty, ty) ty' ->
            try unify env ty ty' with Unify trace ->
@@ -198,6 +211,7 @@ let transl_simple_type_delayed env styp =
   used_variables := Tbl.empty;
   bindings := [];
   (typ,
+(* XXX L'unification peut echouer... *)
    function () -> List.iter (function (t1, t2) -> unify env t1 t2) b)
 
 let transl_type_scheme env styp =
diff --git a/typing/typetexp.mli b/typing/typetexp.mli
index 14dc9a3bc4..ca711321f2 100644
--- a/typing/typetexp.mli
+++ b/typing/typetexp.mli
@@ -24,6 +24,8 @@ val transl_type_scheme:
 val reset_type_variables: unit -> unit
 val enter_type_variable: bool -> string -> Types.type_expr
 val type_variable : Location.t -> string -> Types.type_expr
+val narrow: unit -> unit
+val widen: unit -> unit
 
 exception Already_bound