TT.contract (xlate_term f st lenv) t
let mk_contents n tt = function
- | T.Decl -> [], E.Abst (n, tt)
- | T.Ax -> [], E.Abst (n, tt)
- | T.Cong -> [], E.Abst (n, tt)
- | T.Def -> [], E.Abbr tt
- | T.Th -> [], E.Abbr tt
+ | T.Decl -> [] , E.Abst (n, tt)
+ | T.Ax -> [E.InProp] , E.Abst (n, tt)
+ | T.Cong -> [E.InProp; E.Progress], E.Abst (n, tt)
+ | T.Def -> [] , E.Abbr tt
+ | T.Th -> [E.InProp] , E.Abbr tt
let xlate_entity err f gen st = function
- | T.Require _ ->
+ | T.Require _ ->
err st
- | T.Section (Some name) ->
+ | T.Section (Some name) ->
err {st with path = name :: st.path}
- | T.Section None ->
+ | T.Section None ->
begin match st.path with
| _ :: ptl ->
err {st with path = ptl}
| _ -> assert false
end
- | T.Sorts sorts ->
+ | T.Sorts sorts ->
let map st (xix, s) =
let ix = match xix with
| None -> st.sort
{st with sort = H.set_sorts ix [s]}
in
err (List.fold_left map st sorts)
- | T.Graph id ->
+ | T.Graph id ->
assert (H.set_graph id); err st
- | T.Entity (kind, n, id, meta, t) ->
+ | T.Entity (main, kind, n, id, info, t) ->
let uri = uri_of_id st id st.path in
Hashtbl.add henv id uri;
let tt = xlate_term C.start st D.empty_lenv t in
(*
print_newline (); CrgOutput.pp_term print_string tt;
*)
- let a, b = mk_contents n tt kind in
- let a = if meta <> "" then E.Meta meta :: a else a in
+ let a = [] in
+ let ms, b = mk_contents n tt kind in
+ let ms = if main then E.Main :: ms else ms in
+ let a = if ms <> [] then E.Meta ms :: a else a in
+ let a = if info <> ("", "") then E.Info info :: a else a in
let entity = E.Mark st.line :: a, uri, b in
f {st with line = succ st.line} entity
- | T.Generate _ ->
+ | T.Generate _ ->
err st
(* Interface functions ******************************************************)