X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fdual_rg%2Fdrg.ml;h=e598a59867d40eb0adf175bfe9c35f324b2a4e74;hb=552427acaacc2ebd0737c2b6038085f7ea5f423b;hp=1d94a26437708f409a98f2a5520097554471fd0a;hpb=099f9169edb36348a13f85ebe71c39d44703a696;p=helm.git

diff --git a/helm/software/lambda-delta/dual_rg/drg.ml b/helm/software/lambda-delta/dual_rg/drg.ml
index 1d94a2643..e598a5986 100644
--- a/helm/software/lambda-delta/dual_rg/drg.ml
+++ b/helm/software/lambda-delta/dual_rg/drg.ml
@@ -28,9 +28,8 @@ and term = Sort of attrs * int              (* attrs, hierarchy index *)
          | LRef of attrs * int              (* attrs, position index *)
          | GRef of attrs * uri              (* attrs, reference *)
          | Cast of attrs * term * term      (* attrs, domain, element *)
-         | Proj of attrs * lenv * term      (* attrs, closure, scope *)
          | Appl of attrs * term list * term (* attrs, arguments, function *)
-	 | Bind of bind * term              (* binder, scope *)
+	 | Bind of lenv * term              (* closure, scope *)
 
 and lenv = bind list (* local environment *)