- conditional compilation continues ...

[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 7a6600898b3def2e7321114dd93f9374bbf9b7f7..5a726ca9703b732041fe5a0f0f09ef5536de5890 100644 (file)
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -212,7 +212,9 @@ let xlate_entity err f st lst = function
 *)
                let na = E.node_attrs ~apix:lst.line () in
               let entity = E.empty_root, na, uri_of_qid qid, E.Abst t in
-               G.set_current_trace lst.line;
+IFDEF TRACE THEN
+               G.set_current_trace lst.line
+ELSE () END;
               f {lst with line = succ lst.line} entity
            in
            xlate_term f st lst true lenv w
@@ -234,7 +236,9 @@ let xlate_entity err f st lst = function
                   let na = E.node_attrs ~apix:lst.line () 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, E.Abbr t in
-                  G.set_current_trace lst.line;
+IFDEF TRACE THEN
+                  G.set_current_trace lst.line
+ELSE () END;
                  f {lst with line = succ lst.line} entity
               in
               xlate_term f st lst false lenv v