Shared definition of [binding].

generator/print_coq.ml

@@ -117,6 +117,13 @@ let label = function
 
 (* -------------------------------------------------------------------------- *)
 
+(* Bindings, or annotations: [x : t]. *)
+
+let binding x t =
+  block (x ^^ spacecolon) (space ^^ t) empty
+
+(* -------------------------------------------------------------------------- *)
+
 (* Expressions. *)
 
 let rec expr0 = function
@@ -137,7 +144,7 @@ let rec expr0 = function
   | Coq_record _les ->
       assert false (* TODO *)
   | Coq_annot (e1, e2) ->
-      parens (expr e1 ^^ spacecolon ^/^ expr e2)
+      parens (binding (expr e1) (expr e2))
   | Coq_app _
   | Coq_tag _
   | Coq_impl _
@@ -230,6 +237,14 @@ and mod_typ2 = function
 and mod_typ mt =
   mod_typ1 mt
 
+(* Module bindings. *)
+
+let mod_binding (xs, mt) = 
+  binding (separate_map space string xs) (mod_typ mt)
+
+let mod_bindings bs = 
+  separate_map space mod_binding bs
+
 (* -------------------------------------------------------------------------- *)
 
 (* Typed variables: [x : t]. *)
@@ -237,7 +252,7 @@ and mod_typ mt =
 (* Raw. *)
 
 let var (x, t) =
-  block (string x ^^ spacecolon) (space ^^ expr t) empty
+  binding (string x) (expr t)
 
 (* With parentheses and with a leading space. *)