]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/dual_rg/drg.ml
xml: first ld to xml stylesheets
[helm.git] / helm / software / lambda-delta / dual_rg / drg.ml
index 1d94a26437708f409a98f2a5520097554471fd0a..e598a59867d40eb0adf175bfe9c35f324b2a4e74 100644 (file)
@@ -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 *)