From: Ferruccio Guidi Date: Mon, 10 Nov 2014 17:31:39 +0000 (+0000) Subject: the commit continues with some refactoring ... X-Git-Tag: make_still_working~801 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d6d8c70140357a4ed1f42a2f941234e26752e4dc;p=helm.git the commit continues with some refactoring ... --- diff --git a/helm/software/helena/src/basic_rg/brgType.mli b/helm/software/helena/src/basic_rg/brgType.mli index 169267662..dd8e9a8f6 100644 --- a/helm/software/helena/src/basic_rg/brgType.mli +++ b/helm/software/helena/src/basic_rg/brgType.mli @@ -9,8 +9,6 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -type message = (BrgReduction.kam, Brg.term) Log.message - val type_of: - (message -> 'a) -> (Brg.term -> Brg.term -> 'a) -> + (BrgReduction.message -> 'a) -> (Brg.term -> Brg.term -> 'a) -> Status.status -> BrgReduction.kam -> Brg.term -> 'a