new options activated

[helm.git] / helm / software / helena / src / automath / autCrg.ml

diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index c17b83f07a8f477e189518b84c580b59ccc86d33..667b18cc1bfaea0c77f68dca895ed06d38a871d2 100644 (file)
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -118,7 +118,7 @@ let rec xlate_term f st lst y lenv = function
       let a = E.node_attrs ~sort:h () in
       f a (D.TSort (a, h))
    | A.Appl (v, t)       ->
-      let f vv at tt = f at (D.TAppl (at, vv, tt)) in
+      let f vv at tt = f at (D.TAppl (at, !G.extended, vv, tt)) in
       let f _ vv = xlate_term (f vv) st lst y lenv t in
       xlate_term f st lst false lenv v
    | A.Abst (name, w, t) ->
@@ -146,15 +146,15 @@ let rec xlate_term f st lst y lenv = function
    | A.GRef (name, args) ->
       let map1 args (id, _) = A.GRef ((id, true, []), []) :: args in
       let map2 f arg args = 
-         let f _ arg = f (D.EAppl (args, E.empty_node, arg)) in 
+         let f _ arg = f (D.EAppl (args, E.empty_node, !G.extended, arg)) in 
          xlate_term f st lst false lenv arg
       in
       let g qid a cnt =
          let gref = D.TGRef (a, uri_of_qid qid) in
         if cnt = D.ESort then f a gref else
         let f = function 
-            | D.EAppl (D.ESort, _, v) -> f a (D.TAppl (a, v, gref))
-            | args                    -> f a (D.TProj (a, args, gref))
+            | D.EAppl (D.ESort, _, x, v) -> f a (D.TAppl (a, x, v, gref))
+            | args                       -> f a (D.TProj (a, args, gref))
          in
         let f args = C.list_fold_right f map2 args D.ESort in
         D.sub_list_strict (D.fold_names f map1 args) cnt args
@@ -201,6 +201,7 @@ let xlate_entity err f st lst = function
 *)
               let b = E.Abst t in
               let entity = E.empty_root, aw, uri_of_qid qid, b in
+               G.set_current_trace lst.line;
               f {lst with line = succ lst.line} entity
            in
            xlate_term f st lst true lenv w
@@ -222,6 +223,7 @@ let xlate_entity err f st lst = function
                  let b = E.Abbr t in
                   let ra = if trans then E.empty_root else E.root_attrs ~meta:[E.Private] () in
                  let entity = ra, na, uri_of_qid qid, b in
+                  G.set_current_trace lst.line;
                  f {lst with line = succ lst.line} entity
               in
               xlate_term f st lst false lenv v