]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/toplevel/metaOutput.ml
basic_rg: reduction was not tail recursive by mistake
[helm.git] / helm / software / lambda-delta / toplevel / metaOutput.ml
index caf3cc960deeec33e9c922a2ca0ca1924d8efaf8..21d735d0e187f3f366fc25a475739fa0a84ffeed 100644 (file)
@@ -83,6 +83,7 @@ let count_entity f c = function
       let f c = count_xterm f c xv in
       let f c = count_term f c w in
       Cps.list_fold_left f count_par c pars
+   | _, _, Y.Void               -> assert false
 
 let print_counters f c =
    let terms = c.tsorts + c.tlrefs + c.tgrefs + c.tappls + c.tabsts in
@@ -155,6 +156,7 @@ let pp_entity frm = function
       F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!" 
          (Y.mark C.err C.start a) (U.string_of_uri uri) 
         pp_pars pars (pp_body a) body pp_term u
+   | _, _, Y.Void                   -> assert false
 
 let pp_entity f frm entity =
    pp_entity frm entity; f ()