From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 5 Sep 2009 11:37:27 +0000 (+0000)
Subject: basic_rg: more improvements to the error reporting interface
X-Git-Tag: make_still_working~3495
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ae52a8447fbe67847eba356d26b568d637c90652;p=helm.git

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 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 ->