basic_rg: more improvements to the error reporting interface

diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt
index 90af5cfdc6d84de1a29148be0c5802f24f2ec8f1..6524ef593e30bee91693a67a6b16e95ef069c682 100644 (file)
--- 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 08630cde61865bb923944a09fd8f6d309def6fd2..c8d8ddde9917060288ad5cc3694042539525d016 100644 (file)
--- 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 7515967cd71520a93c9be988bd8eb36e0995d7fa..2ad3bc522eb5039c1d2e11f6979e792c501b4bb8 100644 (file)
--- 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 96c9cb52ab01051f91ac7ac868816504be339eda..d2d6706b830e6a66e656f707654f35be6f6461ad 100644 (file)
--- 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 b9117a3a1dc5280b40f9852cd1125e8ee3ee3a15..6ee5d57edbb804f4acca3d281235fcd272677a60 100644 (file)
--- 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 ->