]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgReduction.mli
helena: warning removed and modifications for λΥP exportation
[helm.git] / helm / software / helena / src / basic_rg / brgReduction.mli
index 85df402838562175f3354d4c3177fee99c60d7cf..50935000a217c1cff364f82515f1b6a2219cae2b 100644 (file)
@@ -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