module T = Types
+module UM = UriManager
module NP = CicNotationPp
module GP = GrafiteAstPp
module G = GrafiteAst
let require value =
command_of_obj (G.Include (floc, value ^ ".ma"))
+let coercion value =
+ command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0))
+
let inline value =
command_of_macro (G.Inline (floc, value))
let commit = function
| T.Heading heading -> out_preamble och heading
| T.Line line -> out_line_comment och line
- | T.BaseUri baseuri -> out_command och (set "baseuri" baseuri)
- | T.Include inc -> out_unexported och "INCLUDE" inc (**)
- | T.Coercion coercion -> out_unexported och "COERCION" coercion (**)
+ | T.BaseUri uri -> out_command och (set "baseuri" uri)
+ | T.Include script -> out_command och (require script)
+ | T.Coercion uri -> out_command och (coercion uri)
| T.Notation notation -> out_unexported och "NOTATION" notation (**)
- | T.Inline (_, uri) -> out_command och (inline uri)
+ | T.Inline specs -> out_command och (inline (snd specs))
| T.Comment comment -> out_comment och comment
| T.Unexport unexport -> out_unexported och "UNEXPORTED" unexport
| T.Verbatim verbatim -> out_verbatim och verbatim