- bug fix in the RTM

[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 c38e8532c203fd28b7f34ee353e906bdde8b582e..866f383417b680e131f573c617b032802276eea2 100644 (file)
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -126,12 +126,13 @@ let rec xlate_term f st lst y lenv = function
       let name = Some (name, true) in
       let f aw ww = 
          let f at tt =
-            let l = if !G.cc then match y, at.E.n_degr with
-               | true, _ -> N.one
-               | _   , 0 -> N.one
-               | _   , 1 -> N.unknown st
-               | _   , 2 -> N.two
-               | _       -> assert false
+            let l = 
+               if !G.cc then match y, at.E.n_degr with
+                  | true, _ -> N.one
+                  | _   , 0 -> N.one
+                  | _   , 1 -> N.unknown st
+                  | _   , 2 -> N.two
+                  | _       -> assert false
                else N.infinite
             in
            let b = D.Abst (l, ww) in
@@ -206,7 +207,7 @@ let xlate_entity err f st lst = function
         in
          complete_qid f lst (name, true, [])
       in
-      get_cnt_relaxed (D.sta f) lst
+      get_cnt_relaxed (D.replace f N.one) lst
    | A.Def (name, w, trans, v) ->
       let f lenv =
          let f qid = 
@@ -239,7 +240,7 @@ let initial_status () =
 }
 
 let refresh_status lst = {lst with
-   mk_uri = G.get_mk_uri ()
+   mk_uri = G.get_mk_uri (); line = 1;
 }
 
 let crg_of_aut = xlate_entity