X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fautomath%2FautCrg.ml;fp=helm%2Fsoftware%2Fhelena%2Fsrc%2Fautomath%2FautCrg.ml;h=5ed896306dfcf0558d6858ad499f57398b3f94f0;hb=bcc6a96020485731da4c02cc38043817903bd7dc;hp=f597f6cf1db3fb8e306d8e1112543990b6e9074a;hpb=bc4a1cafaf3ffa471483210da7b076feeed7c0dc;p=helm.git

diff --git a/helm/software/helena/src/automath/autCrg.ml b/helm/software/helena/src/automath/autCrg.ml
index f597f6cf1..5ed896306 100644
--- a/helm/software/helena/src/automath/autCrg.ml
+++ b/helm/software/helena/src/automath/autCrg.ml
@@ -114,11 +114,17 @@ let get_cnt_relaxed f lst =
 let push_abst f y w lenv =
    let bw = D.Abst (false, N.infinity, w) in
    D.push_bind f E.empty_node y bw lenv
-
+(*
+let rec set_name_y f = function
+   | D.ESort              -> f D.ESort
+   | D.EBind (e, a, y, b) -> set_name_y (D.push_bind f a {y with E.b_name = Some ("Y", true)} b) e
+   | D.EAppl (e, x, v)    -> set_name_y (D.push_appl f x v) e
+   | D.EProj (e, d)       -> let f d = set_name_y (D.push_proj f d) e in set_name_y f d
+*)
 let add_proj yt e t = match e with
    | D.ESort                    -> t
    | D.EBind (D.ESort, _, y, b) -> D.TBind (E.compose y yt, b, t) 
-   | _                          ->
+   | e                          ->
       D.TProj (D.set_attrs C.start yt e, t)
 
 (* this is not tail recursive in the GRef branch *)
@@ -148,6 +154,7 @@ let rec xlate_term f st lst z lenv = function
                else N.infinity
             in
 	    let b = D.Abst (false, l, ww) in
+(*            let yt = {yt with E.b_name = Some ("P", true)} in *)
 	    f yt (D.TBind (yt, b, tt))
 	 in
          let f lenv = xlate_term f st lst z lenv t in