- bug fix in the static analyzer allows better Pi/forall separation (exportation...

[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 b2d0c99e1630aa54641e6cbeb1561e41ebb573ca..1ba830669610da12bf40f36fbf134c48f9b24078 100644 (file)
--- a/helm/software/helena/src/text/txtCrg.ml
+++ b/helm/software/helena/src/text/txtCrg.ml
@@ -66,7 +66,7 @@ let rec xlate_term f st lenv = function
    Printf.printf "\n";
 *)
    | T.Sort h         ->
-      let a = E.node_attrs ~sort:h () in 
+      let a = E.node_attrs ~main:(h, 0) () in 
       f a (D.TSort (a, h))
    | T.NSrt id        ->
       let f h = xlate_term f st lenv (T.Sort h) in
@@ -115,7 +115,7 @@ and xlate_bind st f (lenv, e) b =
          in
          xlate_term f st lenv v
       | T.Void id           ->
-         let a = E.node_attrs ?name:(name_of_id id) ~sort:st.sort () in
+         let a = E.node_attrs ?name:(name_of_id id) ~main:(st.sort, 0) () in
          f a D.Void
 
 let mk_contents main kind tt =