]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_rg/brgOutput.mli
- common/entity: new format for kernel entities
[helm.git] / helm / software / lambda-delta / basic_rg / brgOutput.mli
index 0af895dd454c61b77f5bb5e53d0b73617c7ea46a..69700febdf838508b551e0c2c017323616170d74 100644 (file)
@@ -19,4 +19,4 @@ val print_counters: (unit -> 'a) -> counters -> 'a
 
 val specs: (Brg.lenv, Brg.term) Log.specs
 
-val export_entry: Format.formatter -> Brg.bind Entity.entry -> unit
+val export_term: Format.formatter -> Brg.term -> unit