Commit 9c87f55b authored by POTTIER Francois's avatar POTTIER Francois

Untested function [mod_typ].

parent ec10070b
......@@ -197,6 +197,41 @@ and expr e =
(* -------------------------------------------------------------------------- *)
(* Module types. *)
let rec mod_typ0 = function
| Mod_typ_var x ->
string x
| Mod_typ_app _
| Mod_typ_with_def _
| Mod_typ_with_mod _
as mt ->
parens (mod_typ mt)
and mod_typ1 = function
| Mod_typ_app xs ->
separate_map space string xs
| mt ->
mod_typ0 mt
and mod_typ2 = function
| Mod_typ_with_def (mt, x, e) ->
mod_typ2 mt ^/^
block
(string "with Definition " ^^ string x ^^ space ^^ colonequals)
(break 1 ^^ expr e)
empty
| Mod_typ_with_mod (mt, x, y) ->
mod_typ2 mt ^/^
sprintf "with Module %s := %s " x y
| mt ->
mod_typ1 mt
and mod_typ mt =
mod_typ1 mt
(* -------------------------------------------------------------------------- *)
(* Typed variables: [x : t]. *)
(* Raw. *)
......@@ -349,7 +384,7 @@ let tops ts =
(*
| Coqtop_declare_module (x,mt) ->
sprintf "Declare Module %s : %s." x (string_of_mod_typ mt)
sprintf "Declare Module %s : %s." x (mod_typ mt)
| Coqtop_module (x,bs,c,d) ->
sprintf "Module %s %s %s %s" x (string_of_mod_bindings bs) (string_of_mod_cast c) (string_of_mod_def x d)
| Coqtop_module_type (x,bs,d) ->
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment