Synchronize with trunk.

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

16 files changed, 1377 insertions, 342 deletions

diff --git a/experimental/garrigue/caml_set_oid.diffs b/experimental/garrigue/caml_set_oid.diff
index aaaa160ef..aaaa160ef 100644
--- a/experimental/garrigue/caml_set_oid.diffs
+++ b/experimental/garrigue/caml_set_oid.diff
diff --git a/experimental/garrigue/coerce.diffs b/experimental/garrigue/coerce.diff
index e90e1fc93..e90e1fc93 100644
--- a/experimental/garrigue/coerce.diffs
+++ b/experimental/garrigue/coerce.diff
diff --git a/experimental/garrigue/gadt-escape-check.diffs b/experimental/garrigue/gadt-escape-check.diff
index 3e4a44e2b..3e4a44e2b 100644
--- a/experimental/garrigue/gadt-escape-check.diffs
+++ b/experimental/garrigue/gadt-escape-check.diff
diff --git a/experimental/garrigue/marshal_objects.diffs b/experimental/garrigue/marshal_objects.diff
index bb9b4dd71..bb9b4dd71 100644
--- a/experimental/garrigue/marshal_objects.diffs
+++ b/experimental/garrigue/marshal_objects.diff
diff --git a/experimental/garrigue/module-errors.diffs b/experimental/garrigue/module-errors.diff
index 2f8c2bc28..2f8c2bc28 100644
--- a/experimental/garrigue/module-errors.diffs
+++ b/experimental/garrigue/module-errors.diff
diff --git a/experimental/garrigue/multimatch.diffs b/experimental/garrigue/multimatch.diff
index 6eb34b72e..6eb34b72e 100644
--- a/experimental/garrigue/multimatch.diffs
+++ b/experimental/garrigue/multimatch.diff
diff --git a/experimental/garrigue/nongeneral-let.diff b/experimental/garrigue/nongeneral-let.diff
new file mode 100644
index 000000000..bcdc69e84
--- /dev/null
+++ b/experimental/garrigue/nongeneral-let.diff
@@ -0,0 +1,428 @@
+Index: camlp4/Camlp4/Struct/Grammar/Delete.ml
+===================================================================
+--- camlp4/Camlp4/Struct/Grammar/Delete.ml	(revision 14037)
++++ camlp4/Camlp4/Struct/Grammar/Delete.ml	(working copy)
+@@ -35,17 +35,17 @@
+   open Structure;
+ 
+ value raise_rule_not_found entry symbols =
+-  let to_string f x =
++  let to_string : !'a. (_ -> 'a -> _) -> 'a -> _ = fun [f -> fun [x ->
+     let buff = Buffer.create 128 in
+     let ppf = Format.formatter_of_buffer buff in
+     do {
+       f ppf x;
+       Format.pp_print_flush ppf ();
+       Buffer.contents buff
+-    } in
+-    let entry = to_string Print.entry entry in
+-    let symbols = to_string Print.print_rule symbols in
+-    raise (Rule_not_found (symbols, entry))
++    }]] in
++  let entry = to_string Print.entry entry in
++  let symbols = to_string Print.print_rule symbols in
++  raise (Rule_not_found (symbols, entry))
+ ;
+ 
+ (* Deleting a rule *)
+Index: camlp4/boot/Camlp4.ml
+===================================================================
+--- camlp4/boot/Camlp4.ml	(revision 14037)
++++ camlp4/boot/Camlp4.ml	(working copy)
+@@ -18022,7 +18022,7 @@
+                 open Structure
+                   
+                 let raise_rule_not_found entry symbols =
+-                  let to_string f x =
++                  let to_string : 'a. (_ -> 'a -> _) -> 'a -> _ = fun f x ->
+                     let buff = Buffer.create 128 in
+                     let ppf = Format.formatter_of_buffer buff
+                     in
+Index: camlp4/Camlp4Filters/Camlp4FoldGenerator.ml
+===================================================================
+--- camlp4/Camlp4Filters/Camlp4FoldGenerator.ml	(revision 14037)
++++ camlp4/Camlp4Filters/Camlp4FoldGenerator.ml	(working copy)
+@@ -547,14 +547,18 @@
+ 
+   value processor =
+     let last = ref <:ctyp<>> in
+-    let generate_class' generator default c s n =
++    let generate_class'
++      : !'a 'b. (_ -> 'a -> _ -> _ -> 'b) -> 'b -> 'a -> _ -> _ -> 'b =
++      fun generator default c s n ->
+       match s with
+       [ "Fold"    -> generator Fold c last.val n
+       | "Map"     -> generator Map c last.val n
+       | "FoldMap" -> generator Fold_map c last.val n
+       | _ -> default ]
+     in
+-    let generate_class_from_module_name generator c default m =
++    let generate_class_from_module_name
++      : !'a 'b. (_ -> 'a -> _ -> _ -> 'b) -> 'a -> 'b -> _ -> 'b =
++      fun generator c default m ->
+       try Scanf.sscanf m "Camlp4%[^G]Generator" begin fun m' ->
+         try Scanf.sscanf m' "%[^0-9]%d" (generate_class' generator default c)
+         with [ End_of_file | Scanf.Scan_failure _ -> generate_class' generator default c m' 1 ]
+Index: stdlib/arg.ml
+===================================================================
+--- stdlib/arg.ml	(revision 14037)
++++ stdlib/arg.ml	(working copy)
+@@ -106,7 +106,7 @@
+   let l = Array.length argv in
+   let b = Buffer.create 200 in
+   let initpos = !current in
+-  let stop error =
++  let stop : 'a. _ -> 'a = fun error ->
+     let progname = if initpos < l then argv.(initpos) else "(?)" in
+     begin match error with
+       | Unknown "-help" -> ()
+Index: stdlib/printf.ml
+===================================================================
+--- stdlib/printf.ml	(revision 14037)
++++ stdlib/printf.ml	(working copy)
+@@ -492,7 +492,7 @@
+    Don't do this at home, kids. *)
+ let scan_format fmt args n pos cont_s cont_a cont_t cont_f cont_m =
+ 
+-  let get_arg spec n =
++  let get_arg : 'a. _ -> _ -> 'a = fun spec n ->
+     Obj.magic (args.(Sformat.int_of_index (get_index spec n))) in
+ 
+   let rec scan_positional n widths i =
+Index: stdlib/camlinternalOO.ml
+===================================================================
+--- stdlib/camlinternalOO.ml	(revision 14037)
++++ stdlib/camlinternalOO.ml	(working copy)
+@@ -349,7 +349,7 @@
+   init_table.env_init <- env_init
+ 
+ let dummy_class loc =
+-  let undef = fun _ -> raise (Undefined_recursive_module loc) in
++  let undef : 'a 'b.'a -> 'b = fun _ -> raise (Undefined_recursive_module loc) in
+   (Obj.magic undef, undef, undef, Obj.repr 0)
+ 
+ (**** Objects ****)
+@@ -527,7 +527,7 @@
+   | Closure of closure
+ 
+ let method_impl table i arr =
+-  let next () = incr i; magic arr.(!i) in
++  let next : 'a. unit -> 'a = fun () -> incr i; magic arr.(!i) in
+   match next() with
+     GetConst -> let x : t = next() in get_const x
+   | GetVar   -> let n = next() in get_var n
+Index: stdlib/scanf.ml
+===================================================================
+--- stdlib/scanf.ml	(revision 14037)
++++ stdlib/scanf.ml	(working copy)
+@@ -1324,10 +1324,11 @@
+ 
+   let limr = Array.length rv - 1 in
+ 
+-  let return v = Obj.magic v () in
+-  let delay f x () = f x in
+-  let stack f = delay (return f) in
+-  let no_stack f _x = f in
++  let return : 'a 'b 'c. ('a -> 'b) -> 'c = fun v -> Obj.magic v () in
++  let delay : 'a 'b. ('a -> 'b) -> 'a -> unit -> 'b = fun f x () -> f x in
++  let stack : 'a 'b 'd 'e. ('a -> 'b) -> 'd -> unit -> 'e =
++    fun f -> delay (return f) in
++  let no_stack : 'a 'b. 'a -> 'b -> 'a = fun f _x -> f in
+ 
+   let rec scan fmt =
+ 
+@@ -1380,7 +1381,8 @@
+       scan_conversion skip width_opt prec_opt ir f i
+ 
+     and scan_conversion skip width_opt prec_opt ir f i =
+-      let stack = if skip then no_stack else stack in
++      let stack : 'b 'd. (unit -> 'b) -> 'd -> unit -> 'b =
++        if skip then no_stack else stack in
+       let width = int_of_width_opt width_opt in
+       let prec = int_of_prec_opt prec_opt in
+       match Sformat.get fmt i with
+Index: typing/typemod.ml
+===================================================================
+--- typing/typemod.ml	(revision 14037)
++++ typing/typemod.ml	(working copy)
+@@ -420,7 +420,7 @@
+ 
+ (* let signature sg = List.map (fun item -> item.sig_type) sg *)
+ 
+-let rec transl_modtype env smty =
++let rec transl_modtype env smty : Typedtree.module_type =
+   let loc = smty.pmty_loc in
+   match smty.pmty_desc with
+     Pmty_ident lid ->
+@@ -609,7 +609,7 @@
+     List.fold_left
+       (fun env (id, _, mty) -> Env.add_module id mty.mty_type env)
+       env curr in
+-  let transition env_c curr =
++  let transition : 'a. _ -> (_ * _ * 'a) list -> _ = fun env_c curr ->
+     List.map2
+       (fun (_,smty) (id,id_loc,mty) -> (id, id_loc, transl_modtype env_c smty))
+       sdecls curr in
+Index: typing/typecore.ml
+===================================================================
+--- typing/typecore.ml	(revision 14037)
++++ typing/typecore.ml	(working copy)
+@@ -1373,9 +1373,9 @@
+ 
+   let ty_arrow gty ty = newty (Tarrow ("", instance_def gty, ty, Cok)) in
+ 
+-  let bad_conversion fmt i c =
++  let bad_conversion : 'a. string -> int -> char -> 'a = fun fmt i c ->
+     raise (Error (loc, Env.empty, Bad_conversion (fmt, i, c))) in
+-  let incomplete_format fmt =
++  let incomplete_format : 'a. string -> 'a = fun fmt ->
+     raise (Error (loc, Env.empty, Incomplete_format fmt)) in
+ 
+   let rec type_in_format fmt =
+@@ -3238,7 +3238,7 @@
+ 
+ (* Typing of let bindings *)
+ 
+-and type_let ?(check = fun s -> Warnings.Unused_var s)
++and type_let ?(global=false) ?(check = fun s -> Warnings.Unused_var s)
+              ?(check_strict = fun s -> Warnings.Unused_var_strict s)
+     env rec_flag spat_sexp_list scope allow =
+   begin_def();
+@@ -3368,7 +3368,7 @@
+         )
+       pat_list
+   in
+-  let exp_list =
++  let exp_gen_list =
+     List.map2
+       (fun (spat, sexp) (pat, slot) ->
+         let sexp =
+@@ -3386,9 +3386,12 @@
+             let exp = type_expect exp_env sexp ty' in
+             end_def ();
+             check_univars env true "definition" exp pat.pat_type vars;
+-            {exp with exp_type = instance env exp.exp_type}
+-        | _ -> type_expect exp_env sexp pat.pat_type)
++            {exp with exp_type = instance env exp.exp_type}, true
++        | _ ->
++            type_expect exp_env sexp pat.pat_type,
++            match sexp.pexp_desc with Pexp_ident _ -> true | _ -> false)
+       spat_sexp_list pat_slot_list in
++  let exp_list, gen_list = List.split exp_gen_list in
+   current_slot := None;
+   if is_recursive && not !rec_needed
+   && Warnings.is_active Warnings.Unused_rec_flag then
+@@ -3399,10 +3402,12 @@
+     pat_list exp_list;
+   end_def();
+   List.iter2
+-    (fun pat exp ->
+-       if not (is_nonexpansive exp) then
++    (fun pat (exp, gen) ->
++       if not (global || gen) then
++         iter_pattern (fun pat -> generalize_structure pat.pat_type) pat
++       else if not (is_nonexpansive exp) then
+          iter_pattern (fun pat -> generalize_expansive env pat.pat_type) pat)
+-    pat_list exp_list;
++    pat_list exp_gen_list;
+   List.iter
+     (fun pat -> iter_pattern (fun pat -> generalize pat.pat_type) pat)
+     pat_list;
+@@ -3413,7 +3418,7 @@
+ let type_binding env rec_flag spat_sexp_list scope =
+   Typetexp.reset_type_variables();
+   let (pat_exp_list, new_env, unpacks) =
+-    type_let
++    type_let ~global:true
+       ~check:(fun s -> Warnings.Unused_value_declaration s)
+       ~check_strict:(fun s -> Warnings.Unused_value_declaration s)
+       env rec_flag spat_sexp_list scope false
+Index: typing/includecore.ml
+===================================================================
+--- typing/includecore.ml	(revision 14037)
++++ typing/includecore.ml	(working copy)
+@@ -123,7 +123,8 @@
+   | Record_representation of bool
+ 
+ let report_type_mismatch0 first second decl ppf err =
+-  let pr fmt = Format.fprintf ppf fmt in
++  let pr : 'a. ('a, Format.formatter, unit) format -> 'a
++      = fun fmt -> Format.fprintf ppf fmt in
+   match err with
+     Arity -> pr "They have different arities"
+   | Privacy -> pr "A private type would be revealed"
+Index: ocamldoc/odoc_html.ml
+===================================================================
+--- ocamldoc/odoc_html.ml	(revision 14037)
++++ ocamldoc/odoc_html.ml	(working copy)
+@@ -508,7 +508,7 @@
+       bs b "</table>\n"
+ 
+     method html_of_Index_list b =
+-      let index_if_not_empty l url m =
++      let index_if_not_empty : 'a. 'a list -> _ = fun l url m ->
+         match l with
+           [] -> ()
+         | _ -> bp b "<li><a href=\"%s\">%s</a></li>\n" url m
+@@ -977,7 +977,7 @@
+     (** A function to build the header of pages. *)
+     method prepare_header module_list =
+       let f b ?(nav=None) ?(comments=[]) t  =
+-        let link_if_not_empty l m url =
++        let link_if_not_empty : 'a. 'a list -> _ = fun l m url ->
+           match l with
+             [] -> ()
+           | _ ->
+Index: bytecomp/translmod.ml
+===================================================================
+--- bytecomp/translmod.ml	(revision 14037)
++++ bytecomp/translmod.ml	(working copy)
+@@ -773,7 +773,8 @@
+   Lprim(Psetglobal target_name, [Lprim(Pmakeblock(0, Immutable), components)])
+ 
+ let transl_store_package component_names target_name coercion =
+-  let rec make_sequence fn pos arg =
++  let rec make_sequence : 'a. (int -> 'a -> _) -> int -> 'a list -> _ =
++    fun fn pos arg ->
+     match arg with
+       [] -> lambda_unit
+     | hd :: tl -> Lsequence(fn pos hd, make_sequence fn (pos + 1) tl) in
+Index: otherlibs/labltk/jpf/jpf_font.ml
+===================================================================
+--- otherlibs/labltk/jpf/jpf_font.ml	(revision 14037)
++++ otherlibs/labltk/jpf/jpf_font.ml	(working copy)
+@@ -131,7 +131,7 @@
+   }
+ 
+ let string_of_pattern =
+-  let pat f = function
++  let pat : 'a. ('a -> string) -> 'a option -> string = fun f -> function
+       Some x -> f x
+     | None -> "*"
+   in
+Index: otherlibs/labltk/browser/searchid.ml
+===================================================================
+--- otherlibs/labltk/browser/searchid.ml	(revision 14037)
++++ otherlibs/labltk/browser/searchid.ml	(working copy)
+@@ -396,7 +396,7 @@
+ let search_string_symbol text =
+   if text = "" then [] else
+   let lid = snd (longident_of_string text) [] in
+-  let try_lookup f k =
++  let try_lookup : 'a. _ -> 'a -> (_ * 'a) list = fun f k ->
+     try let _ = f lid Env.initial in [lid, k]
+     with Not_found | Env.Error _ -> []
+   in
+Index: otherlibs/labltk/browser/setpath.ml
+===================================================================
+--- otherlibs/labltk/browser/setpath.ml	(revision 14037)
++++ otherlibs/labltk/browser/setpath.ml	(working copy)
+@@ -117,12 +117,12 @@
+   bind_space_toggle dirbox;
+   bind_space_toggle pathbox;
+ 
+-  let add_paths _ =
++  let add_paths : 'a. 'a -> unit = fun _ ->
+     add_to_path pathbox ~base:!current_dir
+       ~dirs:(List.map (Listbox.curselection dirbox)
+               ~f:(fun x -> Listbox.get dirbox ~index:x));
+     Listbox.selection_clear dirbox ~first:(`Num 0) ~last:`End
+-  and remove_paths _ =
++  and remove_paths : 'a. 'a -> unit = fun _ ->
+     remove_path pathbox
+       ~dirs:(List.map (Listbox.curselection pathbox)
+               ~f:(fun x -> Listbox.get pathbox ~index:x))
+Index: otherlibs/labltk/browser/viewer.ml
+===================================================================
+--- otherlibs/labltk/browser/viewer.ml	(revision 14037)
++++ otherlibs/labltk/browser/viewer.ml	(working copy)
+@@ -507,7 +507,8 @@
+       if i < 3 then Listbox.delete box ~first:(`Num 0) ~last:`End
+       else destroy fm
+     done;
+-    let rec firsts n = function [] -> []
++    let rec firsts : 'a. int -> 'a list -> 'a list = fun n -> function
++        [] -> []
+       | a :: l -> if n > 0 then a :: firsts (pred n) l else [] in
+     shown_paths <- firsts (n-1) shown_paths;
+     boxes <- firsts (max 3 n) boxes
+Index: otherlibs/labltk/frx/frx_req.ml
+===================================================================
+--- otherlibs/labltk/frx/frx_req.ml	(revision 14037)
++++ otherlibs/labltk/frx/frx_req.ml	(working copy)
+@@ -40,7 +40,7 @@
+   let e =
+     Entry.create t [Relief Sunken; TextVariable memory; TextWidth len] in
+ 
+-  let activate _ =
++  let activate : 'a. 'a -> unit = fun _ ->
+     let v = Entry.get e in
+      Grab.release t;                    (* because of wm *)
+      destroy t;                         (* so action can call open_simple *)
+@@ -77,7 +77,7 @@
+ 
+   let waiting = Textvariable.create_temporary t in
+ 
+-  let activate _ =
++  let activate : 'a. 'a -> unit = fun _ ->
+      Grab.release t;                    (* because of wm *)
+      destroy t;                         (* so action can call open_simple *)
+      Textvariable.set waiting "1" in
+@@ -125,7 +125,7 @@
+     Listbox.insert lb End elements;
+ 
+   (* activation: we have to break() because we destroy the requester *)
+-  let activate _ =
++  let activate : 'a. 'a -> unit = fun _ ->
+     let l = List.map (Listbox.get lb) (Listbox.curselection lb) in
+     Grab.release t;
+     destroy t;
+Index: otherlibs/labltk/support/rawwidget.ml
+===================================================================
+--- otherlibs/labltk/support/rawwidget.ml	(revision 14037)
++++ otherlibs/labltk/support/rawwidget.ml	(working copy)
+@@ -67,7 +67,7 @@
+ (* This one is always created by opentk *)
+ let default_toplevel =
+   let wname = "." in
+-  let w = Typed (wname, "toplevel") in
++  let w : 'a. 'a raw_widget = Typed (wname, "toplevel") in
+     Hashtbl.add table wname w;
+     w
+ 
+@@ -145,7 +145,7 @@
+           then "." ^ name
+           else parentpath ^ "." ^ name
+     in
+-      let w = Typed(path,clas) in
++      let w :'a. 'a raw_widget = Typed(path,clas) in
+         Hashtbl.add table path w;
+         w
+ 
+Index: ocamlbuild/rule.ml
+===================================================================
+--- ocamlbuild/rule.ml	(revision 14037)
++++ ocamlbuild/rule.ml	(working copy)
+@@ -260,7 +260,8 @@
+                      which is deprecated and ignored."
+           name
+   in
+-  let res_add import xs xopt =
++  let res_add : 'b. ('a -> 'b) -> 'a list -> 'a option -> 'b list =
++    fun import xs xopt ->
+     let init =
+       match xopt with
+       | None -> []
+Index: ocamlbuild/main.ml
+===================================================================
+--- ocamlbuild/main.ml	(revision 14037)
++++ ocamlbuild/main.ml	(working copy)
+@@ -50,7 +50,7 @@
+ let show_documentation () =
+   let rules = Rule.get_rules () in
+   let flags = Flags.get_flags () in
+-  let pp fmt = Log.raw_dprintf (-1) fmt in
++  let pp : 'a. ('a,_,_) format -> 'a = fun fmt -> Log.raw_dprintf (-1) fmt in
+   List.iter begin fun rule ->
+     pp "%a@\n@\n" (Rule.pretty_print Resource.print_pattern) rule
+   end rules;
diff --git a/experimental/garrigue/objvariant.diffs b/experimental/garrigue/objvariant.diff
index 75deb24cd..75deb24cd 100644
--- a/experimental/garrigue/objvariant.diffs
+++ b/experimental/garrigue/objvariant.diff
diff --git a/experimental/garrigue/parser-lessminus.diffs b/experimental/garrigue/parser-lessminus.diff
index 7b535307c..7b535307c 100644
--- a/experimental/garrigue/parser-lessminus.diffs
+++ b/experimental/garrigue/parser-lessminus.diff
diff --git a/experimental/garrigue/pattern-local-types.diffs b/experimental/garrigue/pattern-local-types.diff
index 0e6f00a2e..0e6f00a2e 100644
--- a/experimental/garrigue/pattern-local-types.diffs
+++ b/experimental/garrigue/pattern-local-types.diff
diff --git a/experimental/garrigue/show_types.diff b/experimental/garrigue/show_types.diff
new file mode 100644
index 000000000..f59105ee9
--- /dev/null
+++ b/experimental/garrigue/show_types.diff
@@ -0,0 +1,419 @@
+Index: parsing/printast.mli
+===================================================================
+--- parsing/printast.mli	(revision 13955)
++++ parsing/printast.mli	(working copy)
+@@ -16,3 +16,4 @@
+ val interface : formatter -> signature_item list -> unit;;
+ val implementation : formatter -> structure_item list -> unit;;
+ val top_phrase : formatter -> toplevel_phrase -> unit;;
++val string_of_kind : ident_kind -> string;;
+Index: parsing/pprintast.ml
+===================================================================
+--- parsing/pprintast.ml	(revision 13955)
++++ parsing/pprintast.ml	(working copy)
+@@ -1192,8 +1192,10 @@
+     | Pdir_none -> ()
+     | Pdir_string (s) -> pp f "@ %S" s
+     | Pdir_int (i) -> pp f "@ %d" i
+-    | Pdir_ident (li) -> pp f "@ %a" self#longident li
+-    | Pdir_bool (b) -> pp f "@ %s" (string_of_bool b))
++    | Pdir_ident {txt=li} -> pp f "@ %a" self#longident li
++    | Pdir_bool (b) -> pp f "@ %s" (string_of_bool b)
++    | Pdir_show (k, {txt=li}) ->
++        pp f "@ %s %a" (Printast.string_of_kind k) self#longident li)
+ 
+   method toplevel_phrase f x =
+     match x with
+Index: parsing/parser.mly
+===================================================================
+--- parsing/parser.mly	(revision 13955)
++++ parsing/parser.mly	(working copy)
+@@ -516,9 +516,9 @@
+   | SEMISEMI EOF                                { [] }
+   | SEMISEMI seq_expr use_file_tail             { Ptop_def[mkstrexp $2] :: $3 }
+   | SEMISEMI structure_item use_file_tail       { Ptop_def[$2] :: $3 }
+-  | SEMISEMI toplevel_directive use_file_tail   { $2 :: $3 }
+   | structure_item use_file_tail                { Ptop_def[$1] :: $2 }
+-  | toplevel_directive use_file_tail            { $1 :: $2 }
++  | SEMISEMI toplevel_directive SEMISEMI use_file_tail   { $2 :: $4 }
++  | toplevel_directive SEMISEMI use_file_tail            { $1 :: $3 }
+ ;
+ 
+ /* Module expressions */
+@@ -1779,16 +1779,26 @@
+   | FALSE                                       { Lident "false" }
+   | TRUE                                        { Lident "true" }
+ ;
++ident_kind:
++    VAL                                         { Pkind_val }
++  | TYPE                                        { Pkind_type }
++  | EXCEPTION                                   { Pkind_exception }
++  | MODULE                                      { Pkind_module }
++  | MODULE TYPE                                 { Pkind_modtype }
++  | CLASS                                       { Pkind_class }
++  | CLASS TYPE                                  { Pkind_cltype }
++;
+ 
+ /* Toplevel directives */
+ 
+ toplevel_directive:
+-    SHARP ident                 { Ptop_dir($2, Pdir_none) }
+-  | SHARP ident STRING          { Ptop_dir($2, Pdir_string $3) }
+-  | SHARP ident INT             { Ptop_dir($2, Pdir_int $3) }
+-  | SHARP ident val_longident   { Ptop_dir($2, Pdir_ident $3) }
+-  | SHARP ident FALSE           { Ptop_dir($2, Pdir_bool false) }
+-  | SHARP ident TRUE            { Ptop_dir($2, Pdir_bool true) }
++    SHARP ident                                 { Ptop_dir($2, Pdir_none) }
++  | SHARP ident STRING                          { Ptop_dir($2, Pdir_string $3) }
++  | SHARP ident INT                             { Ptop_dir($2, Pdir_int $3) }
++  | SHARP ident val_longident                   { Ptop_dir($2, Pdir_ident (mkrhs $3 3)) }
++  | SHARP ident ident_kind any_longident        { Ptop_dir($2, Pdir_show ($3, mkrhs $4 4)) }
++  | SHARP ident FALSE                           { Ptop_dir($2, Pdir_bool false) }
++  | SHARP ident TRUE                            { Ptop_dir($2, Pdir_bool true) }
+ ;
+ 
+ /* Miscellaneous */
+Index: parsing/parsetree.mli
+===================================================================
+--- parsing/parsetree.mli	(revision 13955)
++++ parsing/parsetree.mli	(working copy)
+@@ -294,6 +294,15 @@
+ 
+ (* Toplevel phrases *)
+ 
++type ident_kind =
++    Pkind_val
++  | Pkind_type
++  | Pkind_exception
++  | Pkind_module
++  | Pkind_modtype
++  | Pkind_class
++  | Pkind_cltype
++
+ type toplevel_phrase =
+     Ptop_def of structure
+   | Ptop_dir of string * directive_argument
+@@ -302,5 +311,6 @@
+     Pdir_none
+   | Pdir_string of string
+   | Pdir_int of int
+-  | Pdir_ident of Longident.t
++  | Pdir_ident of Longident.t Location.loc
++  | Pdir_show of ident_kind * Longident.t Location.loc
+   | Pdir_bool of bool
+Index: parsing/printast.ml
+===================================================================
+--- parsing/printast.ml	(revision 13955)
++++ parsing/printast.ml	(working copy)
+@@ -737,6 +737,16 @@
+       core_type (i+1) ppf ct
+ ;;
+ 
++let string_of_kind = function
++    Pkind_val -> "val"
++  | Pkind_type -> "type"
++  | Pkind_exception -> "exception"
++  | Pkind_module -> "module"
++  | Pkind_modtype -> "module type"
++  | Pkind_class -> "class"
++  | Pkind_cltype -> "class type"
++;;
++
+ let rec toplevel_phrase i ppf x =
+   match x with
+   | Ptop_def (s) ->
+@@ -751,7 +761,9 @@
+   | Pdir_none -> line i ppf "Pdir_none\n"
+   | Pdir_string (s) -> line i ppf "Pdir_string \"%s\"\n" s;
+   | Pdir_int (i) -> line i ppf "Pdir_int %d\n" i;
+-  | Pdir_ident (li) -> line i ppf "Pdir_ident %a\n" fmt_longident li;
++  | Pdir_ident {txt=li} -> line i ppf "Pdir_ident %a\n" fmt_longident li;
++  | Pdir_show (kind,{txt=li}) ->
++      line i ppf "Pdir_show %s %a\n" (string_of_kind kind) fmt_longident li;
+   | Pdir_bool (b) -> line i ppf "Pdir_bool %s\n" (string_of_bool b);
+ ;;
+ 
+Index: toplevel/opttoploop.ml
+===================================================================
+--- toplevel/opttoploop.ml	(revision 13955)
++++ toplevel/opttoploop.ml	(working copy)
+@@ -53,6 +53,7 @@
+    | Directive_string of (string -> unit)
+    | Directive_int of (int -> unit)
+    | Directive_ident of (Longident.t -> unit)
++   | Directive_show of (ident_kind -> Longident.t -> unit)
+    | Directive_bool of (bool -> unit)
+ 
+ 
+@@ -270,6 +271,7 @@
+         | (Directive_string f, Pdir_string s) -> f s; true
+         | (Directive_int f, Pdir_int n) -> f n; true
+         | (Directive_ident f, Pdir_ident lid) -> f lid; true
++        | (Directive_show f, Pdir_show (kind,lid)) -> f kind lid; true
+         | (Directive_bool f, Pdir_bool b) -> f b; true
+         | (_, _) ->
+             fprintf ppf "Wrong type of argument for directive `%s'.@." dir_name;
+Index: toplevel/topdirs.ml
+===================================================================
+--- toplevel/topdirs.ml	(revision 13955)
++++ toplevel/topdirs.ml	(working copy)
+@@ -15,6 +15,7 @@
+ open Format
+ open Misc
+ open Longident
++open Parsetree
+ open Types
+ open Cmo_format
+ open Trace
+@@ -191,9 +192,9 @@
+   Ctype.generalize ty_arg;
+   ty_arg
+ 
+-let find_printer_type ppf lid =
++let find_printer_type ppf {Location.loc; txt=lid} =
+   try
+-    let (path, desc) = Env.lookup_value lid !toplevel_env in
++    let (path, desc) = Typetexp.find_value !toplevel_env loc lid in
+     let (ty_arg, is_old_style) =
+       try
+         (match_printer_type ppf desc "printer_type_new", false)
+@@ -201,12 +202,12 @@
+         (match_printer_type ppf desc "printer_type_old", true) in
+     (ty_arg, path, is_old_style)
+   with
+-  | Not_found ->
+-      fprintf ppf "Unbound value %a.@." Printtyp.longident lid;
++    Typetexp.Error _ as exn ->
++      Errors.report_error ppf exn;
+       raise Exit
+   | Ctype.Unify _ ->
+       fprintf ppf "%a has a wrong type for a printing function.@."
+-      Printtyp.longident lid;
++        Printtyp.longident lid;
+       raise Exit
+ 
+ let dir_install_printer ppf lid =
+@@ -227,7 +228,7 @@
+     begin try
+       remove_printer path
+     with Not_found ->
+-      fprintf ppf "No printer named %a.@." Printtyp.longident lid
++      fprintf ppf "No printer named %a.@." Printtyp.longident lid.Location.txt
+     end
+   with Exit -> ()
+ 
+@@ -244,9 +245,9 @@
+   get_code_pointer
+     (Obj.repr (fun arg -> Trace.print_trace (current_environment()) arg))
+ 
+-let dir_trace ppf lid =
++let dir_trace ppf {Location.loc; txt=lid} =
+   try
+-    let (path, desc) = Env.lookup_value lid !toplevel_env in
++    let (path, desc) = Typetexp.find_value !toplevel_env loc lid in
+     (* Check if this is a primitive *)
+     match desc.val_kind with
+     | Val_prim p ->
+@@ -278,11 +279,11 @@
+             fprintf ppf "%a is now traced.@." Printtyp.longident lid
+         end else fprintf ppf "%a is not a function.@." Printtyp.longident lid
+   with
+-  | Not_found -> fprintf ppf "Unbound value %a.@." Printtyp.longident lid
++    Typetexp.Error _ as exn -> Errors.report_error ppf exn
+ 
+-let dir_untrace ppf lid =
++let dir_untrace ppf {Location.loc; txt=lid} =
+   try
+-    let (path, desc) = Env.lookup_value lid !toplevel_env in
++    let (path, desc) = Typetexp.find_value !toplevel_env loc lid in
+     let rec remove = function
+     | [] ->
+         fprintf ppf "%a was not traced.@." Printtyp.longident lid;
+@@ -295,7 +296,7 @@
+         end else f :: remove rem in
+     traced_functions := remove !traced_functions
+   with
+-  | Not_found -> fprintf ppf "Unbound value %a.@." Printtyp.longident lid
++    Typetexp.Error _ as exn -> Errors.report_error ppf exn
+ 
+ let dir_untrace_all ppf () =
+   List.iter
+@@ -305,10 +306,74 @@
+     !traced_functions;
+   traced_functions := []
+ 
++(* Warnings *)
++
+ let parse_warnings ppf iserr s =
+   try Warnings.parse_options iserr s
+   with Arg.Bad err -> fprintf ppf "%s.@." err
+ 
++(* Typing information *)
++
++let rec trim_modtype = function
++    Mty_signature _ -> Mty_signature []
++  | Mty_functor (id, mty, mty') ->
++      Mty_functor (id, mty, trim_modtype mty')
++  | Mty_ident _ as mty -> mty
++
++let trim_signature = function
++    Mty_signature sg ->
++      Mty_signature
++        (List.map
++           (function
++               Sig_module (id, mty, rs) ->
++                 Sig_module (id, trim_modtype mty, rs)
++             (*| Sig_modtype (id, Modtype_manifest mty) ->
++                 Sig_modtype (id, Modtype_manifest (trim_modtype mty))*)
++             | item -> item)
++           sg)
++  | mty -> mty
++
++let dir_show ppf kind {Location.loc; txt=lid} =
++  let env = !Toploop.toplevel_env in
++  try
++    let id =
++      let s = match lid with
++        Longident.Lident s -> s
++      | Longident.Ldot (_,s) -> s
++      | Longident.Lapply _ -> failwith "invalid"
++      in Ident.create_persistent s
++    in
++    let item =
++      match kind with
++        Pkind_val ->
++          let path, desc = Typetexp.find_value env loc lid in
++          Sig_value (id, desc)
++      | Pkind_type ->
++          let path, desc = Typetexp.find_type env loc lid in
++          Sig_type (id, desc, Trec_not)
++      | Pkind_exception ->
++          let desc = Typetexp.find_constructor env loc lid in
++          Sig_exception (id, {exn_args=desc.cstr_args; exn_loc=Location.none})
++      | Pkind_module ->
++          let path, desc = Typetexp.find_module env loc lid in
++          Sig_module (id, trim_signature desc, Trec_not)
++      | Pkind_modtype ->
++          let path, desc = Typetexp.find_modtype env loc lid in
++          Sig_modtype (id, desc)
++      | Pkind_class ->
++          let path, desc = Typetexp.find_class env loc lid in
++          Sig_class (id, desc, Trec_not)
++      | Pkind_cltype ->
++          let path, desc = Typetexp.find_class_type env loc lid in
++          Sig_class_type (id, desc, Trec_not)
++    in
++    fprintf ppf "%a@." Printtyp.signature [item]
++  with
++    Not_found ->
++      fprintf ppf "Unknown %s.@." (Printast.string_of_kind kind)
++  | Failure "invalid" ->
++      fprintf ppf "Invalid path %a@." Printtyp.longident lid
++
+ let _ =
+   Hashtbl.add directive_table "trace" (Directive_ident (dir_trace std_out));
+   Hashtbl.add directive_table "untrace" (Directive_ident (dir_untrace std_out));
+@@ -337,4 +402,7 @@
+              (Directive_string (parse_warnings std_out false));
+ 
+   Hashtbl.add directive_table "warn_error"
+-             (Directive_string (parse_warnings std_out true))
++             (Directive_string (parse_warnings std_out true));
++
++  Hashtbl.add directive_table "show"
++             (Directive_show (dir_show std_out))
+Index: toplevel/toploop.ml
+===================================================================
+--- toplevel/toploop.ml	(revision 13955)
++++ toplevel/toploop.ml	(working copy)
+@@ -25,7 +25,8 @@
+    | Directive_none of (unit -> unit)
+    | Directive_string of (string -> unit)
+    | Directive_int of (int -> unit)
+-   | Directive_ident of (Longident.t -> unit)
++   | Directive_ident of (Longident.t Location.loc -> unit)
++   | Directive_show of (ident_kind -> Longident.t Location.loc -> unit)
+    | Directive_bool of (bool -> unit)
+ 
+ (* The table of toplevel value bindings and its accessors *)
+@@ -280,6 +281,7 @@
+         | (Directive_string f, Pdir_string s) -> f s; true
+         | (Directive_int f, Pdir_int n) -> f n; true
+         | (Directive_ident f, Pdir_ident lid) -> f lid; true
++        | (Directive_show f, Pdir_show (kind,lid)) -> f kind lid; true
+         | (Directive_bool f, Pdir_bool b) -> f b; true
+         | (_, _) ->
+             fprintf ppf "Wrong type of argument for directive `%s'.@." dir_name;
+Index: toplevel/topdirs.mli
+===================================================================
+--- toplevel/topdirs.mli	(revision 13955)
++++ toplevel/topdirs.mli	(working copy)
+@@ -20,11 +20,12 @@
+ val dir_cd : string -> unit
+ val dir_load : formatter -> string -> unit
+ val dir_use : formatter -> string -> unit
+-val dir_install_printer : formatter -> Longident.t -> unit
+-val dir_remove_printer : formatter -> Longident.t -> unit
+-val dir_trace : formatter -> Longident.t -> unit
+-val dir_untrace : formatter -> Longident.t -> unit
++val dir_install_printer : formatter -> Longident.t Location.loc -> unit
++val dir_remove_printer : formatter -> Longident.t Location.loc -> unit
++val dir_trace : formatter -> Longident.t Location.loc -> unit
++val dir_untrace : formatter -> Longident.t Location.loc -> unit
+ val dir_untrace_all : formatter -> unit -> unit
++val dir_show : formatter -> Parsetree.ident_kind -> Longident.t Location.loc -> unit
+ 
+ type 'a printer_type_new = Format.formatter -> 'a -> unit
+ type 'a printer_type_old = 'a -> unit
+Index: toplevel/toploop.mli
+===================================================================
+--- toplevel/toploop.mli	(revision 13955)
++++ toplevel/toploop.mli	(working copy)
+@@ -37,7 +37,8 @@
+    | Directive_none of (unit -> unit)
+    | Directive_string of (string -> unit)
+    | Directive_int of (int -> unit)
+-   | Directive_ident of (Longident.t -> unit)
++   | Directive_ident of (Longident.t Location.loc -> unit)
++   | Directive_show of (Parsetree.ident_kind -> Longident.t Location.loc -> unit)
+    | Directive_bool of (bool -> unit)
+ 
+ val directive_table : (string, directive_fun) Hashtbl.t
+Index: tools/Makefile.shared
+===================================================================
+--- tools/Makefile.shared	(revision 13955)
++++ tools/Makefile.shared	(working copy)
+@@ -210,6 +210,7 @@
+           ../parsing/location.cmo \
+           ../parsing/longident.cmo \
+           ../parsing/lexer.cmo \
++          ../parsing/printast.cmo \
+           ../parsing/pprintast.cmo \
+           ../typing/ident.cmo \
+           ../typing/path.cmo \
+Index: camlp4/Camlp4/Struct/Camlp4Ast2OCamlAst.ml
+===================================================================
+--- camlp4/Camlp4/Struct/Camlp4Ast2OCamlAst.ml	(revision 13955)
++++ camlp4/Camlp4/Struct/Camlp4Ast2OCamlAst.ml	(working copy)
+@@ -1229,7 +1229,7 @@
+     | ExInt _ i -> Pdir_int (int_of_string i)
+     | <:expr< True >> -> Pdir_bool True
+     | <:expr< False >> -> Pdir_bool False
+-    | e -> Pdir_ident (ident_noloc (ident_of_expr e)) ]
++    | e -> Pdir_ident (ident (ident_of_expr e)) ]
+   ;
+ 
+   value phrase =
+Index: camlp4/boot/Camlp4.ml
+===================================================================
+--- camlp4/boot/Camlp4.ml	(revision 13955)
++++ camlp4/boot/Camlp4.ml	(working copy)
+@@ -15686,7 +15686,7 @@
+               | ExInt (_, i) -> Pdir_int (int_of_string i)
+               | Ast.ExId (_, (Ast.IdUid (_, "True"))) -> Pdir_bool true
+               | Ast.ExId (_, (Ast.IdUid (_, "False"))) -> Pdir_bool false
+-              | e -> Pdir_ident (ident_noloc (ident_of_expr e))
++              | e -> Pdir_ident (ident (ident_of_expr e))
+               
+             let phrase =
+               function
diff --git a/experimental/garrigue/show_types.diffs b/experimental/garrigue/show_types.diffs
deleted file mode 100644
index 0c2919550..000000000
--- a/experimental/garrigue/show_types.diffs
+++ /dev/null
@@ -1,160 +0,0 @@
-Index: typing/printtyp.ml
-===================================================================
---- typing/printtyp.ml	(revision 11316)
-+++ typing/printtyp.ml	(working copy)
-@@ -894,8 +894,10 @@
-       tree_of_class_declaration id decl rs :: tree_of_signature rem
-   | Tsig_cltype(id, decl, rs) :: tydecl1 :: tydecl2 :: rem ->
-       tree_of_cltype_declaration id decl rs :: tree_of_signature rem
--  | _ ->
--      assert false
-+  | Tsig_class(id, decl, rs) :: _ ->
-+      tree_of_class_declaration id decl rs :: []
-+  | Tsig_cltype(id, decl, rs) :: _ ->
-+      tree_of_cltype_declaration id decl rs :: []
- 
- and tree_of_modtype_declaration id decl =
-   let mty =
-Index: toplevel/topdirs.ml
-===================================================================
---- toplevel/topdirs.ml	(revision 11316)
-+++ toplevel/topdirs.ml	(working copy)
-@@ -297,10 +297,92 @@
-     !traced_functions;
-   traced_functions := []
- 
-+(* Warnings *)
-+
- let parse_warnings ppf iserr s =
-   try Warnings.parse_options iserr s
-   with Arg.Bad err -> fprintf ppf "%s.@." err
- 
-+(* Typing information *)
-+
-+type pkind =
-+    Pvalue
-+  | Ptype
-+  | Pexception
-+  | Pmodule
-+  | Pmodtype
-+  | Pclass
-+  | Pcltype
-+
-+let name_of_kind = function
-+    Pvalue -> "value"
-+  | Ptype -> "type"
-+  | Pexception -> "exception"
-+  | Pmodule -> "module"
-+  | Pmodtype -> "module type"
-+  | Pclass -> "class"
-+  | Pcltype -> "class type"
-+
-+let rec trim_modtype = function
-+    Tmty_signature _ -> Tmty_signature []
-+  | Tmty_functor (id, mty, mty') ->
-+      Tmty_functor (id, mty, trim_modtype mty')
-+  | Tmty_ident _ as mty -> mty
-+
-+let trim_signature = function
-+    Tmty_signature sg ->
-+      Tmty_signature
-+        (List.map
-+           (function
-+               Tsig_module (id, mty, rs) ->
-+                 Tsig_module (id, trim_modtype mty, rs)
-+             (*| Tsig_modtype (id, Tmodtype_manifest mty) ->
-+                 Tsig_modtype (id, Tmodtype_manifest (trim_modtype mty))*)
-+             | item -> item)
-+           sg)
-+  | mty -> mty
-+
-+let show_type ppf kind lid =
-+  let env = !Toploop.toplevel_env in
-+  try
-+    let id =
-+      let s = match lid with
-+        Longident.Lident s -> s
-+      | Longident.Ldot (_,s) -> s
-+      | Longident.Lapply _ -> failwith "invalid"
-+      in Ident.create_persistent s
-+    in
-+    let item =
-+      match kind with
-+        Pvalue ->
-+          let path, desc = Env.lookup_value lid env in
-+          Tsig_value (id, desc)
-+      | Ptype ->
-+          let path, desc = Env.lookup_type lid env in
-+          Tsig_type (id, desc, Trec_not)
-+      | Pexception ->
-+          let desc = Env.lookup_constructor lid env in
-+          Tsig_exception (id, desc.cstr_args)
-+      | Pmodule ->
-+          let path, desc = Env.lookup_module lid env in
-+          Tsig_module (id, trim_signature desc, Trec_not)
-+      | Pmodtype ->
-+          let path, desc = Env.lookup_modtype lid env in
-+          Tsig_modtype (id, desc)
-+      | Pclass ->
-+          let path, desc = Env.lookup_class lid env in
-+          Tsig_class (id, desc, Trec_not)
-+      | Pcltype ->
-+          let path, desc = Env.lookup_cltype lid env in
-+          Tsig_cltype (id, desc, Trec_not)
-+    in
-+    fprintf ppf "%a@." Printtyp.signature [item]
-+  with
-+    Not_found ->
-+      fprintf ppf "Unknown %s.@." (name_of_kind kind)
-+  | Failure "invalid" ->
-+      fprintf ppf "Invalid path %a@." Printtyp.longident lid
-+
- let _ =
-   Hashtbl.add directive_table "trace" (Directive_ident (dir_trace std_out));
-   Hashtbl.add directive_table "untrace" (Directive_ident (dir_untrace std_out));
-@@ -329,4 +411,19 @@
-              (Directive_string (parse_warnings std_out false));
- 
-   Hashtbl.add directive_table "warn_error"
--             (Directive_string (parse_warnings std_out true))
-+             (Directive_string (parse_warnings std_out true));
-+
-+  Hashtbl.add directive_table "show_value"
-+             (Directive_ident (show_type std_out Pvalue));
-+  Hashtbl.add directive_table "show_type"
-+             (Directive_ident (show_type std_out Ptype));
-+  Hashtbl.add directive_table "show_exception"
-+             (Directive_ident (show_type std_out Pexception));
-+  Hashtbl.add directive_table "show_module"
-+             (Directive_ident (show_type std_out Pmodule));
-+  Hashtbl.add directive_table "show_module_type"
-+             (Directive_ident (show_type std_out Pmodtype));
-+  Hashtbl.add directive_table "show_class"
-+             (Directive_ident (show_type std_out Pclass));
-+  Hashtbl.add directive_table "show_class_type"
-+             (Directive_ident (show_type std_out Pcltype))
-Index: parsing/parser.mly
-===================================================================
---- parsing/parser.mly	(revision 11316)
-+++ parsing/parser.mly	(working copy)
-@@ -1769,6 +1769,11 @@
-     LIDENT                                      { Lident $1 }
-   | mod_longident DOT LIDENT                    { Ldot($1, $3) }
- ;
-+any_longident:
-+    val_ident                                   { Lident $1 }
-+  | mod_longident DOT val_ident                 { Ldot($1, $3) }
-+  | mod_longident                               { $1 }
-+;
- 
- /* Toplevel directives */
- 
-@@ -1776,7 +1781,7 @@
-     SHARP ident                 { Ptop_dir($2, Pdir_none) }
-   | SHARP ident STRING          { Ptop_dir($2, Pdir_string $3) }
-   | SHARP ident INT             { Ptop_dir($2, Pdir_int $3) }
--  | SHARP ident val_longident   { Ptop_dir($2, Pdir_ident $3) }
-+  | SHARP ident any_longident   { Ptop_dir($2, Pdir_ident $3) }
-   | SHARP ident FALSE           { Ptop_dir($2, Pdir_bool false) }
-   | SHARP ident TRUE            { Ptop_dir($2, Pdir_bool true) }
- ;
diff --git a/experimental/garrigue/valvirt.diffs b/experimental/garrigue/valvirt.diff
index 2cf55742b..2cf55742b 100644
--- a/experimental/garrigue/valvirt.diffs
+++ b/experimental/garrigue/valvirt.diff
diff --git a/experimental/garrigue/variable-names-Tvar.diffs b/experimental/garrigue/variable-names-Tvar.diff
index 99ff6a247..99ff6a247 100644
--- a/experimental/garrigue/variable-names-Tvar.diffs
+++ b/experimental/garrigue/variable-names-Tvar.diff
diff --git a/experimental/garrigue/with-module-type.diff b/experimental/garrigue/with-module-type.diff
new file mode 100644
index 000000000..2b99c1f9e
--- /dev/null
+++ b/experimental/garrigue/with-module-type.diff
@@ -0,0 +1,530 @@
+Index: typing/typemod.ml
+===================================================================
+--- typing/typemod.ml	(revision 13947)
++++ typing/typemod.ml	(working copy)
+@@ -80,6 +80,9 @@
+       Typedtree.module_expr * Types.module_type) ref
+   = ref (fun env m -> assert false)
+ 
++let transl_modtype_fwd =
++  ref (fun env m -> (assert false : Typedtree.module_type))
++
+ (* Merge one "with" constraint in a signature *)
+ 
+ let rec add_rec_types env = function
+@@ -191,6 +194,21 @@
+           merge env (extract_sig env loc mty) namelist None in
+         (path_concat id path, lid, tcstr),
+         Sig_module(id, Mty_signature newsg, rs) :: rem
++    | (Sig_modtype(id, mtd) :: rem, [s], Pwith_modtype pmty)
++      when Ident.name id = s ->
++        let mty = !transl_modtype_fwd initial_env pmty in
++        let mtd' = Modtype_manifest mty.mty_type in
++        Includemod.modtype_declarations env id mtd' mtd;
++        (Pident id, lid, Twith_modtype (Tmodtype_manifest mty)),
++        Sig_modtype(id, mtd') :: rem
++    | (Sig_modtype(id, mtd) :: rem, [s], Pwith_modtypesubst pmty)
++      when Ident.name id = s ->
++        let mty = !transl_modtype_fwd initial_env pmty in
++        let mtd' = Modtype_manifest mty.mty_type in
++        Includemod.modtype_declarations env id mtd' mtd;
++        real_id := Some id;
++        (Pident id, lid, Twith_modtypesubst (Tmodtype_manifest mty)),
++        rem
+     | (item :: rem, _, _) ->
+         let (cstr, items) = merge (Env.add_item item env) rem namelist row_id
+         in
+@@ -233,6 +251,12 @@
+         let (path, _) = Typetexp.find_module initial_env loc lid.txt in
+         let sub = Subst.add_module id path Subst.identity in
+         Subst.signature sub sg
++    | [s], Pwith_modtypesubst pmty ->
++        let id =
++          match !real_id with None -> assert false | Some id -> id in
++        let mty = !transl_modtype_fwd initial_env pmty in
++        let sub = Subst.add_modtype id mty.mty_type Subst.identity in
++        Subst.signature sub sg
+     | _ ->
+           sg
+     in
+@@ -649,6 +673,8 @@
+   check_recmod_typedecls env2 sdecls dcl2;
+   (dcl2, env2)
+ 
++let () = transl_modtype_fwd := transl_modtype
++
+ (* Try to convert a module expression to a module path. *)
+ 
+ exception Not_a_path
+Index: typing/typedtreeMap.ml
+===================================================================
+--- typing/typedtreeMap.ml	(revision 13947)
++++ typing/typedtreeMap.ml	(working copy)
+@@ -457,6 +457,9 @@
+         | Twith_typesubst decl -> Twith_typesubst (map_type_declaration decl)
+         | Twith_module (path, lid) -> cstr
+         | Twith_modsubst (path, lid) -> cstr
++        | Twith_modtype decl -> Twith_modtype (map_modtype_declaration decl)
++        | Twith_modtypesubst decl ->
++            Twith_modtypesubst (map_modtype_declaration decl)
+     in
+     Map.leave_with_constraint cstr
+ 
+Index: typing/typedtree.ml
+===================================================================
+--- typing/typedtree.ml	(revision 13947)
++++ typing/typedtree.ml	(working copy)
+@@ -255,6 +255,8 @@
+   | Twith_module of Path.t * Longident.t loc
+   | Twith_typesubst of type_declaration
+   | Twith_modsubst of Path.t * Longident.t loc
++  | Twith_modtype of modtype_declaration
++  | Twith_modtypesubst of modtype_declaration
+ 
+ and core_type =
+ (* mutable because of [Typeclass.declare_method] *)
+Index: typing/typedtree.mli
+===================================================================
+--- typing/typedtree.mli	(revision 13947)
++++ typing/typedtree.mli	(working copy)
+@@ -254,6 +254,8 @@
+   | Twith_module of Path.t * Longident.t loc
+   | Twith_typesubst of type_declaration
+   | Twith_modsubst of Path.t * Longident.t loc
++  | Twith_modtype of modtype_declaration
++  | Twith_modtypesubst of modtype_declaration
+ 
+ and core_type =
+ (* mutable because of [Typeclass.declare_method] *)
+Index: typing/includemod.ml
+===================================================================
+--- typing/includemod.ml	(revision 13947)
++++ typing/includemod.ml	(working copy)
+@@ -346,10 +346,10 @@
+ 
+ (* Hide the context and substitution parameters to the outside world *)
+ 
+-let modtypes env mty1 mty2 = modtypes env [] Subst.identity mty1 mty2
+-let signatures env sig1 sig2 = signatures env [] Subst.identity sig1 sig2
+-let type_declarations env id decl1 decl2 =
+-  type_declarations env [] Subst.identity id decl1 decl2
++let modtypes env = modtypes env [] Subst.identity
++let signatures env = signatures env [] Subst.identity
++let type_declarations env = type_declarations env [] Subst.identity
++let modtype_declarations env = modtype_infos env [] Subst.identity
+ 
+ (* Error report *)
+ 
+Index: typing/typedtreeIter.ml
+===================================================================
+--- typing/typedtreeIter.ml	(revision 13947)
++++ typing/typedtreeIter.ml	(working copy)
+@@ -408,6 +408,8 @@
+         | Twith_module _ -> ()
+         | Twith_typesubst decl -> iter_type_declaration decl
+         | Twith_modsubst _ -> ()
++        | Twith_modtype decl -> iter_modtype_declaration decl
++        | Twith_modtypesubst decl -> iter_modtype_declaration decl
+       end;
+       Iter.leave_with_constraint cstr;
+ 
+Index: typing/includemod.mli
+===================================================================
+--- typing/includemod.mli	(revision 13947)
++++ typing/includemod.mli	(working copy)
+@@ -21,6 +21,8 @@
+ val compunit: string -> signature -> string -> signature -> module_coercion
+ val type_declarations:
+       Env.t -> Ident.t -> type_declaration -> type_declaration -> unit
++val modtype_declarations:
++      Env.t -> Ident.t -> modtype_declaration -> modtype_declaration -> unit
+ 
+ type symptom =
+     Missing_field of Ident.t
+Index: typing/printtyped.ml
+===================================================================
+--- typing/printtyped.ml	(revision 13947)
++++ typing/printtyped.ml	(working copy)
+@@ -608,6 +608,12 @@
+       type_declaration (i+1) ppf td;
+   | Twith_module (li,_) -> line i ppf "Pwith_module %a\n" fmt_path li;
+   | Twith_modsubst (li,_) -> line i ppf "Pwith_modsubst %a\n" fmt_path li;
++  | Twith_modtype (td) ->
++      line i ppf "Pwith_modtype\n";
++      modtype_declaration (i+1) ppf td;
++  | Twith_modtypesubst (td) ->
++      line i ppf "Pwith_modtypesubst\n";
++      modtype_declaration (i+1) ppf td;
+ 
+ and module_expr i ppf x =
+   line i ppf "module_expr %a\n" fmt_location x.mod_loc;
+Index: experimental/garrigue/with-module-type.diffs
+===================================================================
+--- experimental/garrigue/with-module-type.diffs	(revision 13947)
++++ experimental/garrigue/with-module-type.diffs	(working copy)
+@@ -1,95 +1,53 @@
+-Index: parsing/parser.mly
+-===================================================================
+---- parsing/parser.mly	(revision 12005)
+-+++ parsing/parser.mly	(working copy)
+-@@ -1504,6 +1504,10 @@
+-       { ($2, Pwith_module $4) }
+-   | MODULE mod_longident COLONEQUAL mod_ext_longident
+-       { ($2, Pwith_modsubst $4) }
+-+  | MODULE TYPE mod_longident EQUAL module_type
+-+      { ($3, Pwith_modtype $5) }
+-+  | MODULE TYPE mod_longident COLONEQUAL module_type
+-+      { ($3, Pwith_modtypesubst $5) }
+- ;
+- with_type_binder:
+-     EQUAL          { Public }
+-Index: parsing/parsetree.mli
+-===================================================================
+---- parsing/parsetree.mli	(revision 12005)
+-+++ parsing/parsetree.mli	(working copy)
+-@@ -239,6 +239,8 @@
+-   | Pwith_module of Longident.t
+-   | Pwith_typesubst of type_declaration
+-   | Pwith_modsubst of Longident.t
+-+  | Pwith_modtype of module_type
+-+  | Pwith_modtypesubst of module_type
+- 
+- (* Value expressions for the module language *)
+- 
+-Index: parsing/printast.ml
+-===================================================================
+---- parsing/printast.ml	(revision 12005)
+-+++ parsing/printast.ml	(working copy)
+-@@ -575,6 +575,12 @@
+-       type_declaration (i+1) ppf td;
+-   | Pwith_module (li) -> line i ppf "Pwith_module %a\n" fmt_longident li;
+-   | Pwith_modsubst (li) -> line i ppf "Pwith_modsubst %a\n" fmt_longident li;
+-+  | Pwith_modtype (mty) ->
+-+      line i ppf "Pwith_modtype\n";
+-+      module_type (i+1) ppf mty;
+-+  | Pwith_modtypesubst (mty) ->
+-+      line i ppf "Pwith_modtype\n";
+-+      module_type (i+1) ppf mty;
+- 
+- and module_expr i ppf x =
+-   line i ppf "module_expr %a\n" fmt_location x.pmod_loc;
+ Index: typing/typemod.ml
+ ===================================================================
+---- typing/typemod.ml	(revision 12005)
++--- typing/typemod.ml	(revision 13947)
+ +++ typing/typemod.ml	(working copy)
+-@@ -74,6 +74,8 @@
+-   : (Env.t -> Parsetree.module_expr -> module_type) ref
++@@ -80,6 +80,9 @@
++       Typedtree.module_expr * Types.module_type) ref
+    = ref (fun env m -> assert false)
+  
+-+let transl_modtype_fwd = ref (fun env m -> assert false)
+++let transl_modtype_fwd =
+++  ref (fun env m -> (assert false : Typedtree.module_type))
+ +
+  (* Merge one "with" constraint in a signature *)
+  
+  let rec add_rec_types env = function
+-@@ -163,6 +165,19 @@
+-         ignore(Includemod.modtypes env newmty mty);
+-         real_id := Some id;
+-         make_next_first rs rem
+-+    | (Tsig_modtype(id, mtd) :: rem, [s], Pwith_modtype pmty)
++@@ -191,6 +194,21 @@
++           merge env (extract_sig env loc mty) namelist None in
++         (path_concat id path, lid, tcstr),
++         Sig_module(id, Mty_signature newsg, rs) :: rem
+++    | (Sig_modtype(id, mtd) :: rem, [s], Pwith_modtype pmty)
+ +      when Ident.name id = s ->
+ +        let mty = !transl_modtype_fwd initial_env pmty in
+-+        let mtd' = Tmodtype_manifest mty in
+++        let mtd' = Modtype_manifest mty.mty_type in
+ +        Includemod.modtype_declarations env id mtd' mtd;
+-+        Tsig_modtype(id, mtd') :: rem
+-+    | (Tsig_modtype(id, mtd) :: rem, [s], Pwith_modtypesubst pmty)
+++        (Pident id, lid, Twith_modtype (Tmodtype_manifest mty)),
+++        Sig_modtype(id, mtd') :: rem
+++    | (Sig_modtype(id, mtd) :: rem, [s], Pwith_modtypesubst pmty)
+ +      when Ident.name id = s ->
+ +        let mty = !transl_modtype_fwd initial_env pmty in
+-+        let mtd' = Tmodtype_manifest mty in
+++        let mtd' = Modtype_manifest mty.mty_type in
+ +        Includemod.modtype_declarations env id mtd' mtd;
+ +        real_id := Some id;
+++        (Pident id, lid, Twith_modtypesubst (Tmodtype_manifest mty)),
+ +        rem
+-     | (Tsig_module(id, mty, rs) :: rem, s :: namelist, _)
+-       when Ident.name id = s ->
+-         let newsg = merge env (extract_sig env loc mty) namelist None in
+-@@ -200,6 +215,12 @@
+-         let (path, _) = Typetexp.find_module initial_env loc lid in
++     | (item :: rem, _, _) ->
++         let (cstr, items) = merge (Env.add_item item env) rem namelist row_id
++         in
++@@ -233,6 +251,12 @@
++         let (path, _) = Typetexp.find_module initial_env loc lid.txt in
+          let sub = Subst.add_module id path Subst.identity in
+          Subst.signature sub sg
+ +    | [s], Pwith_modtypesubst pmty ->
+ +        let id =
+ +          match !real_id with None -> assert false | Some id -> id in
+ +        let mty = !transl_modtype_fwd initial_env pmty in
+-+        let sub = Subst.add_modtype id mty Subst.identity in
+++        let sub = Subst.add_modtype id mty.mty_type Subst.identity in
+ +        Subst.signature sub sg
+      | _ ->
+-         sg
+-   with Includemod.Error explanation ->
+-@@ -499,6 +520,8 @@
++           sg
++     in
++@@ -649,6 +673,8 @@
+    check_recmod_typedecls env2 sdecls dcl2;
+    (dcl2, env2)
+  
+@@ -98,11 +56,51 @@
+  (* Try to convert a module expression to a module path. *)
+  
+  exception Not_a_path
++Index: typing/typedtreeMap.ml
++===================================================================
++--- typing/typedtreeMap.ml	(revision 13947)
+++++ typing/typedtreeMap.ml	(working copy)
++@@ -457,6 +457,9 @@
++         | Twith_typesubst decl -> Twith_typesubst (map_type_declaration decl)
++         | Twith_module (path, lid) -> cstr
++         | Twith_modsubst (path, lid) -> cstr
+++        | Twith_modtype decl -> Twith_modtype (map_modtype_declaration decl)
+++        | Twith_modtypesubst decl ->
+++            Twith_modtypesubst (map_modtype_declaration decl)
++     in
++     Map.leave_with_constraint cstr
++ 
++Index: typing/typedtree.ml
++===================================================================
++--- typing/typedtree.ml	(revision 13947)
+++++ typing/typedtree.ml	(working copy)
++@@ -255,6 +255,8 @@
++   | Twith_module of Path.t * Longident.t loc
++   | Twith_typesubst of type_declaration
++   | Twith_modsubst of Path.t * Longident.t loc
+++  | Twith_modtype of modtype_declaration
+++  | Twith_modtypesubst of modtype_declaration
++ 
++ and core_type =
++ (* mutable because of [Typeclass.declare_method] *)
++Index: typing/typedtree.mli
++===================================================================
++--- typing/typedtree.mli	(revision 13947)
+++++ typing/typedtree.mli	(working copy)
++@@ -254,6 +254,8 @@
++   | Twith_module of Path.t * Longident.t loc
++   | Twith_typesubst of type_declaration
++   | Twith_modsubst of Path.t * Longident.t loc
+++  | Twith_modtype of modtype_declaration
+++  | Twith_modtypesubst of modtype_declaration
++ 
++ and core_type =
++ (* mutable because of [Typeclass.declare_method] *)
+ Index: typing/includemod.ml
+ ===================================================================
+---- typing/includemod.ml	(revision 12005)
++--- typing/includemod.ml	(revision 13947)
+ +++ typing/includemod.ml	(working copy)
+-@@ -326,10 +326,10 @@
++@@ -346,10 +346,10 @@
+  
+  (* Hide the context and substitution parameters to the outside world *)
+  
+@@ -117,11 +115,24 @@
+  
+  (* Error report *)
+  
++Index: typing/typedtreeIter.ml
++===================================================================
++--- typing/typedtreeIter.ml	(revision 13947)
+++++ typing/typedtreeIter.ml	(working copy)
++@@ -408,6 +408,8 @@
++         | Twith_module _ -> ()
++         | Twith_typesubst decl -> iter_type_declaration decl
++         | Twith_modsubst _ -> ()
+++        | Twith_modtype decl -> iter_modtype_declaration decl
+++        | Twith_modtypesubst decl -> iter_modtype_declaration decl
++       end;
++       Iter.leave_with_constraint cstr;
++ 
+ Index: typing/includemod.mli
+ ===================================================================
+---- typing/includemod.mli	(revision 12005)
++--- typing/includemod.mli	(revision 13947)
+ +++ typing/includemod.mli	(working copy)
+-@@ -23,6 +23,8 @@
++@@ -21,6 +21,8 @@
+  val compunit: string -> signature -> string -> signature -> module_coercion
+  val type_declarations:
+        Env.t -> Ident.t -> type_declaration -> type_declaration -> unit
+@@ -130,53 +141,20 @@
+  
+  type symptom =
+      Missing_field of Ident.t
+-Index: testsuite/tests/typing-modules/Test.ml.reference
++Index: typing/printtyped.ml
+ ===================================================================
+---- testsuite/tests/typing-modules/Test.ml.reference	(revision 12005)
+-+++ testsuite/tests/typing-modules/Test.ml.reference	(working copy)
+-@@ -6,4 +6,12 @@
+- #       type -'a t
+- class type c = object method m : [ `A ] t end
+- #   module M : sig val v : (#c as 'a) -> 'a end
+-+#       module type S = sig module type T module F : functor (X : T) -> T end
+-+# module type T0 = sig type t end
+-+# module type S1 = sig module type T = T0 module F : functor (X : T) -> T end
+-+# module type S2 = sig module F : functor (X : T0) -> T0 end
+-+# module type S3 =
+-+  sig
+-+    module F : functor (X : sig type t = int end) -> sig type t = int end
+-+  end
+- # 
+-Index: testsuite/tests/typing-modules/Test.ml.principal.reference
+-===================================================================
+---- testsuite/tests/typing-modules/Test.ml.principal.reference	(revision 12005)
+-+++ testsuite/tests/typing-modules/Test.ml.principal.reference	(working copy)
+-@@ -6,4 +6,12 @@
+- #       type -'a t
+- class type c = object method m : [ `A ] t end
+- #   module M : sig val v : (#c as 'a) -> 'a end
+-+#       module type S = sig module type T module F : functor (X : T) -> T end
+-+# module type T0 = sig type t end
+-+# module type S1 = sig module type T = T0 module F : functor (X : T) -> T end
+-+# module type S2 = sig module F : functor (X : T0) -> T0 end
+-+# module type S3 =
+-+  sig
+-+    module F : functor (X : sig type t = int end) -> sig type t = int end
+-+  end
+- # 
+-Index: testsuite/tests/typing-modules/Test.ml
+-===================================================================
+---- testsuite/tests/typing-modules/Test.ml	(revision 12005)
+-+++ testsuite/tests/typing-modules/Test.ml	(working copy)
+-@@ -9,3 +9,11 @@
+- class type c = object method m : [ `A ] t end;;
+- module M : sig val v : (#c as 'a) -> 'a end =
+-   struct let v x = ignore (x :> c); x end;;
+-+
+-+(* with module type *)
+-+
+-+module type S = sig module type T module F(X:T) : T end;;
+-+module type T0 = sig type t end;;
+-+module type S1 = S with module type T = T0;;
+-+module type S2 = S with module type T := T0;;
+-+module type S3 = S with module type T := sig type t = int end;;
++--- typing/printtyped.ml	(revision 13947)
+++++ typing/printtyped.ml	(working copy)
++@@ -608,6 +608,12 @@
++       type_declaration (i+1) ppf td;
++   | Twith_module (li,_) -> line i ppf "Pwith_module %a\n" fmt_path li;
++   | Twith_modsubst (li,_) -> line i ppf "Pwith_modsubst %a\n" fmt_path li;
+++  | Twith_modtype (td) ->
+++      line i ppf "Pwith_modtype\n";
+++      modtype_declaration (i+1) ppf td;
+++  | Twith_modtypesubst (td) ->
+++      line i ppf "Pwith_modtypesubst\n";
+++      modtype_declaration (i+1) ppf td;
++ 
++ and module_expr i ppf x =
++   line i ppf "module_expr %a\n" fmt_location x.mod_loc;
+Index: parsing/pprintast.ml
+===================================================================
+--- parsing/pprintast.ml	(revision 13947)
++++ parsing/pprintast.ml	(working copy)
+@@ -847,18 +847,28 @@
+                 (self#list self#type_var_option ~sep:"," ~first:"(" ~last:")")
+                 ls self#longident_loc li  self#type_declaration  td
+           | Pwith_module (li2) ->
+-              pp f "module %a =@ %a" self#longident_loc li self#longident_loc li2;
++              pp f "module %a =@ %a"
++                self#longident_loc li self#longident_loc li2
+           | Pwith_typesubst ({ptype_params=ls;_} as td) ->
+               pp f "type@ %a %a :=@ %a"
+                 (self#list self#type_var_option ~sep:"," ~first:"(" ~last:")")
+                 ls self#longident_loc li
+                 self#type_declaration  td
+           | Pwith_modsubst (li2) ->
+-              pp f "module %a :=@ %a" self#longident_loc li self#longident_loc li2 in
++              pp f "module %a :=@ %a"
++                self#longident_loc li self#longident_loc li2
++          | Pwith_modtype mty ->
++              pp f "module type %a =@ %a"
++                self#longident_loc li self#module_type mty
++          | Pwith_modtypesubst mty ->
++              pp f "module type %a :=@ %a"
++                self#longident_loc li self#module_type mty
++        in
+         (match l with
+         | [] -> pp f "@[<hov2>%a@]" self#module_type mt
+         | _ -> pp f "@[<hov2>(%a@ with@ %a)@]"
+-              self#module_type mt (self#list longident_x_with_constraint ~sep:"@ and@ ") l )
++              self#module_type mt
++              (self#list longident_x_with_constraint ~sep:"@ and@ ") l )
+     | Pmty_typeof me ->
+         pp f "@[<hov2>module@ type@ of@ %a@]"
+           self#module_expr me
+Index: parsing/parser.mly
+===================================================================
+--- parsing/parser.mly	(revision 13947)
++++ parsing/parser.mly	(working copy)
+@@ -1506,6 +1506,10 @@
+       { (mkrhs $2 2, Pwith_module (mkrhs $4 4)) }
+   | MODULE UIDENT COLONEQUAL mod_ext_longident
+       { (mkrhs (Lident $2) 2, Pwith_modsubst (mkrhs $4 4)) }
++  | MODULE TYPE mty_longident EQUAL module_type
++      { (mkrhs $3 3, Pwith_modtype $5) }
++  | MODULE TYPE ident COLONEQUAL module_type
++      { (mkrhs (Lident $3) 3, Pwith_modtypesubst $5) }
+ ;
+ with_type_binder:
+     EQUAL          { Public }
+Index: parsing/ast_mapper.ml
+===================================================================
+--- parsing/ast_mapper.ml	(revision 13947)
++++ parsing/ast_mapper.ml	(working copy)
+@@ -164,6 +164,8 @@
+     | Pwith_module s -> Pwith_module (map_loc sub s)
+     | Pwith_typesubst d -> Pwith_typesubst (sub # type_declaration d)
+     | Pwith_modsubst s -> Pwith_modsubst (map_loc sub s)
++    | Pwith_modtype m -> Pwith_modtype (sub # module_type m)
++    | Pwith_modtypesubst m -> Pwith_modtypesubst (sub # module_type m)
+ 
+   let mk_item ?(loc = Location.none) x = {psig_desc = x; psig_loc = loc}
+ 
+Index: parsing/parsetree.mli
+===================================================================
+--- parsing/parsetree.mli	(revision 13947)
++++ parsing/parsetree.mli	(working copy)
+@@ -256,6 +256,8 @@
+   | Pwith_module of Longident.t loc
+   | Pwith_typesubst of type_declaration
+   | Pwith_modsubst of Longident.t loc
++  | Pwith_modtype of module_type
++  | Pwith_modtypesubst of module_type
+ 
+ (* Value expressions for the module language *)
+ 
+Index: parsing/printast.ml
+===================================================================
+--- parsing/printast.ml	(revision 13947)
++++ parsing/printast.ml	(working copy)
+@@ -590,6 +590,12 @@
+       type_declaration (i+1) ppf td;
+   | Pwith_module li -> line i ppf "Pwith_module %a\n" fmt_longident_loc li;
+   | Pwith_modsubst li -> line i ppf "Pwith_modsubst %a\n" fmt_longident_loc li;
++  | Pwith_modtype (mty) ->
++      line i ppf "Pwith_modtype\n";
++      module_type (i+1) ppf mty;
++  | Pwith_modtypesubst (mty) ->
++      line i ppf "Pwith_modtype\n";
++      module_type (i+1) ppf mty;
+ 
+ and module_expr i ppf x =
+   line i ppf "module_expr %a\n" fmt_location x.pmod_loc;
diff --git a/experimental/garrigue/with-module-type.diffs b/experimental/garrigue/with-module-type.diffs
deleted file mode 100644
index c955b1f86..000000000
--- a/experimental/garrigue/with-module-type.diffs
+++ /dev/null
@@ -1,182 +0,0 @@
-Index: parsing/parser.mly
-===================================================================
---- parsing/parser.mly	(revision 12005)
-+++ parsing/parser.mly	(working copy)
-@@ -1504,6 +1504,10 @@
-       { ($2, Pwith_module $4) }
-   | MODULE mod_longident COLONEQUAL mod_ext_longident
-       { ($2, Pwith_modsubst $4) }
-+  | MODULE TYPE mod_longident EQUAL module_type
-+      { ($3, Pwith_modtype $5) }
-+  | MODULE TYPE mod_longident COLONEQUAL module_type
-+      { ($3, Pwith_modtypesubst $5) }
- ;
- with_type_binder:
-     EQUAL          { Public }
-Index: parsing/parsetree.mli
-===================================================================
---- parsing/parsetree.mli	(revision 12005)
-+++ parsing/parsetree.mli	(working copy)
-@@ -239,6 +239,8 @@
-   | Pwith_module of Longident.t
-   | Pwith_typesubst of type_declaration
-   | Pwith_modsubst of Longident.t
-+  | Pwith_modtype of module_type
-+  | Pwith_modtypesubst of module_type
- 
- (* Value expressions for the module language *)
- 
-Index: parsing/printast.ml
-===================================================================
---- parsing/printast.ml	(revision 12005)
-+++ parsing/printast.ml	(working copy)
-@@ -575,6 +575,12 @@
-       type_declaration (i+1) ppf td;
-   | Pwith_module (li) -> line i ppf "Pwith_module %a\n" fmt_longident li;
-   | Pwith_modsubst (li) -> line i ppf "Pwith_modsubst %a\n" fmt_longident li;
-+  | Pwith_modtype (mty) ->
-+      line i ppf "Pwith_modtype\n";
-+      module_type (i+1) ppf mty;
-+  | Pwith_modtypesubst (mty) ->
-+      line i ppf "Pwith_modtype\n";
-+      module_type (i+1) ppf mty;
- 
- and module_expr i ppf x =
-   line i ppf "module_expr %a\n" fmt_location x.pmod_loc;
-Index: typing/typemod.ml
-===================================================================
---- typing/typemod.ml	(revision 12005)
-+++ typing/typemod.ml	(working copy)
-@@ -74,6 +74,8 @@
-   : (Env.t -> Parsetree.module_expr -> module_type) ref
-   = ref (fun env m -> assert false)
- 
-+let transl_modtype_fwd = ref (fun env m -> assert false)
-+
- (* Merge one "with" constraint in a signature *)
- 
- let rec add_rec_types env = function
-@@ -163,6 +165,19 @@
-         ignore(Includemod.modtypes env newmty mty);
-         real_id := Some id;
-         make_next_first rs rem
-+    | (Tsig_modtype(id, mtd) :: rem, [s], Pwith_modtype pmty)
-+      when Ident.name id = s ->
-+        let mty = !transl_modtype_fwd initial_env pmty in
-+        let mtd' = Tmodtype_manifest mty in
-+        Includemod.modtype_declarations env id mtd' mtd;
-+        Tsig_modtype(id, mtd') :: rem
-+    | (Tsig_modtype(id, mtd) :: rem, [s], Pwith_modtypesubst pmty)
-+      when Ident.name id = s ->
-+        let mty = !transl_modtype_fwd initial_env pmty in
-+        let mtd' = Tmodtype_manifest mty in
-+        Includemod.modtype_declarations env id mtd' mtd;
-+        real_id := Some id;
-+        rem
-     | (Tsig_module(id, mty, rs) :: rem, s :: namelist, _)
-       when Ident.name id = s ->
-         let newsg = merge env (extract_sig env loc mty) namelist None in
-@@ -200,6 +215,12 @@
-         let (path, _) = Typetexp.find_module initial_env loc lid in
-         let sub = Subst.add_module id path Subst.identity in
-         Subst.signature sub sg
-+    | [s], Pwith_modtypesubst pmty ->
-+        let id =
-+          match !real_id with None -> assert false | Some id -> id in
-+        let mty = !transl_modtype_fwd initial_env pmty in
-+        let sub = Subst.add_modtype id mty Subst.identity in
-+        Subst.signature sub sg
-     | _ ->
-         sg
-   with Includemod.Error explanation ->
-@@ -499,6 +520,8 @@
-   check_recmod_typedecls env2 sdecls dcl2;
-   (dcl2, env2)
- 
-+let () = transl_modtype_fwd := transl_modtype
-+
- (* Try to convert a module expression to a module path. *)
- 
- exception Not_a_path
-Index: typing/includemod.ml
-===================================================================
---- typing/includemod.ml	(revision 12005)
-+++ typing/includemod.ml	(working copy)
-@@ -326,10 +326,10 @@
- 
- (* Hide the context and substitution parameters to the outside world *)
- 
--let modtypes env mty1 mty2 = modtypes env [] Subst.identity mty1 mty2
--let signatures env sig1 sig2 = signatures env [] Subst.identity sig1 sig2
--let type_declarations env id decl1 decl2 =
--  type_declarations env [] Subst.identity id decl1 decl2
-+let modtypes env = modtypes env [] Subst.identity
-+let signatures env = signatures env [] Subst.identity
-+let type_declarations env = type_declarations env [] Subst.identity
-+let modtype_declarations env = modtype_infos env [] Subst.identity
- 
- (* Error report *)
- 
-Index: typing/includemod.mli
-===================================================================
---- typing/includemod.mli	(revision 12005)
-+++ typing/includemod.mli	(working copy)
-@@ -23,6 +23,8 @@
- val compunit: string -> signature -> string -> signature -> module_coercion
- val type_declarations:
-       Env.t -> Ident.t -> type_declaration -> type_declaration -> unit
-+val modtype_declarations:
-+      Env.t -> Ident.t -> modtype_declaration -> modtype_declaration -> unit
- 
- type symptom =
-     Missing_field of Ident.t
-Index: testsuite/tests/typing-modules/Test.ml.reference
-===================================================================
---- testsuite/tests/typing-modules/Test.ml.reference	(revision 12005)
-+++ testsuite/tests/typing-modules/Test.ml.reference	(working copy)
-@@ -6,4 +6,12 @@
- #       type -'a t
- class type c = object method m : [ `A ] t end
- #   module M : sig val v : (#c as 'a) -> 'a end
-+#       module type S = sig module type T module F : functor (X : T) -> T end
-+# module type T0 = sig type t end
-+# module type S1 = sig module type T = T0 module F : functor (X : T) -> T end
-+# module type S2 = sig module F : functor (X : T0) -> T0 end
-+# module type S3 =
-+  sig
-+    module F : functor (X : sig type t = int end) -> sig type t = int end
-+  end
- # 
-Index: testsuite/tests/typing-modules/Test.ml.principal.reference
-===================================================================
---- testsuite/tests/typing-modules/Test.ml.principal.reference	(revision 12005)
-+++ testsuite/tests/typing-modules/Test.ml.principal.reference	(working copy)
-@@ -6,4 +6,12 @@
- #       type -'a t
- class type c = object method m : [ `A ] t end
- #   module M : sig val v : (#c as 'a) -> 'a end
-+#       module type S = sig module type T module F : functor (X : T) -> T end
-+# module type T0 = sig type t end
-+# module type S1 = sig module type T = T0 module F : functor (X : T) -> T end
-+# module type S2 = sig module F : functor (X : T0) -> T0 end
-+# module type S3 =
-+  sig
-+    module F : functor (X : sig type t = int end) -> sig type t = int end
-+  end
- # 
-Index: testsuite/tests/typing-modules/Test.ml
-===================================================================
---- testsuite/tests/typing-modules/Test.ml	(revision 12005)
-+++ testsuite/tests/typing-modules/Test.ml	(working copy)
-@@ -9,3 +9,11 @@
- class type c = object method m : [ `A ] t end;;
- module M : sig val v : (#c as 'a) -> 'a end =
-   struct let v x = ignore (x :> c); x end;;
-+
-+(* with module type *)
-+
-+module type S = sig module type T module F(X:T) : T end;;
-+module type T0 = sig type t end;;
-+module type S1 = S with module type T = T0;;
-+module type S2 = S with module type T := T0;;
-+module type S3 = S with module type T := sig type t = int end;;