short names

[helm.git] / helm / software / lambda-delta / dual_rg / drgOutput.ml

diff --git a/helm/software/lambda-delta/dual_rg/drgOutput.ml b/helm/software/lambda-delta/dual_rg/drgOutput.ml
index c291cbf8a60df19827974e34f8f5c237d3e70210..2522b59f14df0446ee8f582f2e9860a1ae12bdfd 100644 (file)
--- a/helm/software/lambda-delta/dual_rg/drgOutput.ml
+++ b/helm/software/lambda-delta/dual_rg/drgOutput.ml
@@ -12,6 +12,7 @@
 module X = Library
 module D = Drg
 
+(* this is not tail recursive *)
 let rec list_iter map l f = match l with
    | []       -> f
    | hd :: tl -> map hd (list_iter map tl f)
@@ -21,6 +22,7 @@ let rec lenv_iter map1 map2 l f = match l with
    | D.EBind (lenv, a, b) -> lenv_iter map1 map2 lenv (map1 a b f)
    | D.EProj (lenv, a, e) -> lenv_iter map1 map2 lenv (map2 a e f)
 
+(* these are not tail recursive *)
 let rec exp_term t f = match t with
    | D.TSort (a, h)       ->
       let attrs = [X.position h; X.name a] in