From: Ferruccio Guidi Date: Sat, 26 Dec 2015 19:06:41 +0000 (+0000) Subject: minor bug fixes ... X-Git-Tag: make_still_working~669 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bcc6a96020485731da4c02cc38043817903bd7dc;p=helm.git minor bug fixes ... --- 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