update in helena

[helm.git] / helm / software / helena / src / text / txtCrg.ml

diff --git a/helm/software/helena/src/text/txtCrg.ml b/helm/software/helena/src/text/txtCrg.ml
index 174857d435875adc2ba22a5bea38b9bcb9ef083d..4580d2d867eb7b29ec5dbf4de2e5b3da5129deae 100644 (file)
--- a/helm/software/helena/src/text/txtCrg.ml
+++ b/helm/software/helena/src/text/txtCrg.ml
@@ -25,7 +25,7 @@ type status = {
    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 *) 
 }
 
@@ -81,7 +81,7 @@ let rec xlate_term f st lenv = function
       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)   ->
@@ -90,7 +90,7 @@ let rec xlate_term f st lenv = function
       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
@@ -120,11 +120,11 @@ and xlate_bind st f (lenv, e) b =
 
 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
 
@@ -171,7 +171,7 @@ let xlate_entity err f gen st = function
 
 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