Matitaweb: layout change in the matitaweb inteface, in order to allow better

[helm.git] / helm / software / lambda-delta / src / complete_rg / crgOutput.ml

diff --git a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml
index c8d3bad88ec4448ba8590f2ad993e6f6eccd8fde..072073c18538793318798c13c08923db68b9e904 100644 (file)
--- a/helm/software/lambda-delta/src/complete_rg/crgOutput.ml
+++ b/helm/software/lambda-delta/src/complete_rg/crgOutput.ml
@@ -44,11 +44,6 @@ let initial_counters = {
    uris = []; nodes = 0; xnodes = 0
 }
 
-let rec shift t = function
-   | D.ESort           -> t
-   | D.EBind (e, a, b) -> shift (D.TBind (a, b, t)) e
-   | D.EProj (e, a, d) -> shift (D.TProj (a, d, t)) e
-
 let rec count_term f c e = function
    | D.TSort _          -> 
       f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
@@ -75,7 +70,7 @@ let rec count_term f c e = function
       let f c = count_term f c e t in
       C.list_fold_right f (map1 e) vs c
    | D.TProj (a, d, t)  ->
-      count_term f c e (shift t d)
+      count_term f c e (D.tshift d t)
    | D.TBind (a, b, t)  -> 
       let f c e = count_term f c e t in
       count_binder f c e a b
@@ -147,8 +142,8 @@ let pp_attrs out a =
       | E.Name (s, false) -> out (P.sprintf "~%s;" s)
       | E.Apix i          -> out (P.sprintf "+%i;" i)
       | E.Mark i          -> out (P.sprintf "@%i;" i)
-      | E.Meta s          -> out (P.sprintf "\"%s\";" s)
-      | E.Priv            -> out (P.sprintf "%s;" "~")
+      | E.Meta _          -> ()
+      | E.Info _          -> ()
    in
    List.iter map a