let command_of_macro macro =
G.Executable (floc, G.Macro (floc, macro))
-let require value =
- command_of_obj (G.Include (floc, value ^ ".ma"))
+let require moo value =
+ command_of_obj (G.Include (floc, moo, `OldAndNew, value ^ ".ma"))
let coercion value =
command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0, 0))
let commit kind och items =
let trd (_, _, x) = x in
let commit = function
- | T.Heading heading -> out_preamble och heading
- | T.Line line ->
+ | T.Heading heading -> out_preamble och heading
+ | T.Line line ->
if !O.comments then out_line_comment och line
- | T.Include script -> out_command och (require script)
- | T.Coercion specs ->
+ | T.Include (moo, script) -> out_command och (require moo script)
+ | T.Coercion specs ->
if !O.comments then out_unexported och "COERCION" (snd specs)
- | T.Notation specs ->
+ | T.Notation specs ->
if !O.comments then out_unexported och "NOTATION" (snd specs) (**)
| T.Inline (_, T.Var, src, _, _, _) ->
if !O.comments then out_unexported och "UNEXPORTED" src