From ae52a8447fbe67847eba356d26b568d637c90652 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 5 Sep 2009 11:37:27 +0000 Subject: [PATCH] basic_rg: more improvements to the error reporting interface --- helm/software/lambda-delta/.depend.opt | 4 ++-- helm/software/lambda-delta/basic_rg/brgReduction.ml | 2 -- helm/software/lambda-delta/basic_rg/brgReduction.mli | 2 -- helm/software/lambda-delta/basic_rg/brgType.ml | 4 +++- helm/software/lambda-delta/basic_rg/brgType.mli | 4 +++- 5 files changed, 8 insertions(+), 8 deletions(-) diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt index 90af5cfdc..6524ef593 100644 --- a/helm/software/lambda-delta/.depend.opt +++ b/helm/software/lambda-delta/.depend.opt @@ -58,8 +58,8 @@ basic_rg/brgReduction.cmo: lib/share.cmx common/output.cmi lib/nUri.cmi \ basic_rg/brgReduction.cmx: lib/share.cmx common/output.cmx lib/nUri.cmx \ lib/log.cmx lib/cps.cmx basic_rg/brgOutput.cmx \ basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgReduction.cmi -basic_rg/brgType.cmi: common/hierarchy.cmi basic_rg/brgReduction.cmi \ - basic_rg/brg.cmx +basic_rg/brgType.cmi: lib/log.cmi common/hierarchy.cmi \ + basic_rg/brgReduction.cmi basic_rg/brg.cmx basic_rg/brgType.cmo: lib/share.cmx lib/nUri.cmi lib/log.cmi \ common/hierarchy.cmi lib/cps.cmx basic_rg/brgSubstitution.cmi \ basic_rg/brgReduction.cmi basic_rg/brgOutput.cmi \ diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml index 08630cde6..c8d8ddde9 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml @@ -24,8 +24,6 @@ type machine = { i: int } -type message = (machine, B.term) Log.item list - (* Internal functions *******************************************************) let level = 5 diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.mli b/helm/software/lambda-delta/basic_rg/brgReduction.mli index 7515967cd..2ad3bc522 100644 --- a/helm/software/lambda-delta/basic_rg/brgReduction.mli +++ b/helm/software/lambda-delta/basic_rg/brgReduction.mli @@ -24,6 +24,4 @@ val are_convertible: (unit -> 'a) -> (unit -> 'a) -> ?si:bool -> machine -> Brg.term -> machine -> Brg.term -> 'a -type message = (machine, Brg.term) Log.item list - val specs: (machine, Brg.term) Log.specs diff --git a/helm/software/lambda-delta/basic_rg/brgType.ml b/helm/software/lambda-delta/basic_rg/brgType.ml index 96c9cb52a..d2d6706b8 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.ml +++ b/helm/software/lambda-delta/basic_rg/brgType.ml @@ -20,7 +20,9 @@ module E = BrgEnvironment module S = BrgSubstitution module R = BrgReduction -exception TypeError of R.message +type message = (R.machine, B.term) Log.item list + +exception TypeError of message (* Internal functions *******************************************************) diff --git a/helm/software/lambda-delta/basic_rg/brgType.mli b/helm/software/lambda-delta/basic_rg/brgType.mli index b9117a3a1..6ee5d57ed 100644 --- a/helm/software/lambda-delta/basic_rg/brgType.mli +++ b/helm/software/lambda-delta/basic_rg/brgType.mli @@ -9,7 +9,9 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -exception TypeError of BrgReduction.message +type message = (BrgReduction.machine, Brg.term) Log.item list + +exception TypeError of message val type_of: (Brg.term -> Brg.term -> 'a) -> ?si:bool -> -- 2.39.2