path : T.id list; (* current section path *)
line : int; (* line number *)
sort : int; (* first default sort index *)
- ext : bool; (* extended applications *)
+ rest : bool; (* restricted applications *)
mk_uri: G.uri_generator (* uri generator *)
}
let f _ uu = xlate_term (f uu) st lenv t in
xlate_term f st lenv u
| T.Appl (v, t) ->
- let f vv y tt = f y (D.TAppl (st.ext, vv, tt)) in
+ let f vv y tt = f y (D.TAppl (E.appl_attrs st.rest, vv, tt)) in
let f _ vv = xlate_term (f vv) st lenv t in
xlate_term f st lenv v
| T.Proj (bs, t) ->
C.list_fold_left f (xlate_bind st) (lenv, D.empty_lenv) bs
| T.Inst (t, vs) ->
let map f v e =
- let f _ vv = D.push_appl f st.ext vv e in
+ let f _ vv = D.push_appl f (E.appl_attrs st.rest) vv e in
xlate_term f st lenv v
in
let f e y tt = f y (D.TProj (e, tt)) in
let mk_contents main kind tt =
let ms, b = match kind with
- | T.Decl -> [] , E.Abst tt
- | T.Ax -> [E.InProp] , E.Abst tt
- | T.Cong -> [E.InProp; E.Progress], E.Abst tt
- | T.Def -> [] , E.Abbr tt
- | T.Th -> [E.InProp] , E.Abbr tt
+ | T.Decl -> [] , E.abst E.empty_env tt
+ | T.Ax -> [E.InProp] , E.abst E.empty_env tt
+ | T.Cong -> [E.InProp; E.Progress], E.abst E.empty_env tt
+ | T.Def -> [] , E.abbr E.empty_env tt
+ | T.Th -> [E.InProp] , E.abbr E.empty_env tt
in
if main then E.Main :: ms, b else ms, b
let initial_status () =
KH.clear henv; {
- path = []; line = 1; sort = 0; ext = false; mk_uri = G.get_mk_uri ()
+ path = []; line = 1; sort = 0; rest = true; mk_uri = G.get_mk_uri ()
}
let refresh_status st = {st with