we are optimizing the code by conditional compilation.

[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 22b3e799c2474bda8996b46f40b905e58ec15014..637aa4a89ceec68233bae4a0584f90a12b764976 100644 (file)
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -119,8 +119,11 @@ let add_proj at e t = match e with
    | D.ESort                 -> t
    | D.EBind (D.ESort, a, b) -> D.TBind (E.compose a at, b, t) 
    | _                       ->
-      let e = if !G.export || !G.manager <> G.Quiet then D.set_attrs C.start at e else e in
+IFDEF MANAGER OR OBJS THEN
+      D.TProj (at, D.set_attrs C.start at e, t)
+ELSE
       D.TProj (at, e, t)
+END
 
 (* this is not tail recursive in the GRef branch *)
 let rec xlate_term f st lst y lenv = function
@@ -170,8 +173,11 @@ let rec xlate_term f st lst y lenv = function
                let a = E.compose av a in
                f a (D.TAppl (a, x, v, gref))
             | args                        ->
-               let args = if !G.export || !G.manager <> G.Quiet then D.set_attrs C.start a args else args in
+IFDEF MANAGER OR OBJS THEN
+               f a (D.TProj (a, D.set_attrs C.start a args, gref))
+ELSE               
                f a (D.TProj (a, args, gref))
+END
          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