X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgReduction.mli;h=50935000a217c1cff364f82515f1b6a2219cae2b;hb=9b1b59a049935f5382ed7def91b807bbf9453894;hp=85df402838562175f3354d4c3177fee99c60d7cf;hpb=30eb28f8c35d7667b3a0052c30d2750a492fa464;p=helm.git

diff --git a/helm/software/helena/src/basic_rg/brgReduction.mli b/helm/software/helena/src/basic_rg/brgReduction.mli
index 85df40283..50935000a 100644
--- a/helm/software/helena/src/basic_rg/brgReduction.mli
+++ b/helm/software/helena/src/basic_rg/brgReduction.mli
@@ -17,12 +17,12 @@ val empty_rtm: rtm
 
 val get: rtm -> int -> Brg.bind
 
-val push: rtm -> Entity.node_attrs -> Brg.bind -> rtm
+val push: rtm -> Entity.bind_attrs -> Brg.bind -> rtm
 
-val xwhd: Status.status -> rtm -> int option -> Brg.term -> rtm * Brg.term 
+val xwhd: Layer.status -> rtm -> int option -> Brg.term -> rtm * Brg.term 
 
 (* arguments: expected type, inferred type *) 
 val are_convertible: 
-   Status.status -> rtm -> int option -> Brg.term -> rtm -> int option -> Brg.term -> bool
+   Layer.status -> rtm -> int option -> Brg.term -> rtm -> int option -> Brg.term -> bool
 
-val specs: (Level.status, rtm, Brg.term) Log.specs
+val specs: (Layer.status, rtm, Brg.term) Log.specs