- dependencies between statuses simplified

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml
index 58a241e3fdc782511125d882e823350d5f4449fb..7511e02aaad65670504ea7a23cd0902990da0148 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.ml
+++ b/matita/components/grafite_parser/grafiteDisambiguate.ml
@@ -28,16 +28,14 @@
 class type g_status =
   object
    inherit LexiconTypes.g_status
-   inherit NCicCoercion.g_status
   end
 
 class status =
  object (self)
   inherit LexiconTypes.status
-  inherit NCicCoercion.status
   method set_grafite_disambiguate_status
    : 'status. #g_status as 'status -> 'self
-      = fun o -> (self#set_lexicon_engine_status o)#set_coercion_status o
+      = fun o -> (self#set_lexicon_engine_status o)
  end
 
 exception BaseUriNotSetYet

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli
index 0074b291668f9690936b5571ccc39aa7e0bb5d3e..6caf5301f200f0f8c667ae5bf534dd5ae8e6c63f 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.mli
+++ b/matita/components/grafite_parser/grafiteDisambiguate.mli
@@ -25,28 +25,15 @@
 
 exception BaseUriNotSetYet
 
-class type g_status =
- object
-  inherit LexiconTypes.g_status
-  inherit NCicCoercion.g_status
- end
-
-class status :
- object ('self)
-  inherit LexiconTypes.status
-  inherit NCicCoercion.status
-  method set_grafite_disambiguate_status: #g_status -> 'self
- end
-
 val disambiguate_nterm :
  NCic.term option -> 
- (#status as 'status) ->
+ (#LexiconTypes.status as 'status) ->
  NCic.context -> NCic.metasenv -> NCic.substitution ->
  NotationPt.term Disambiguate.disambiguator_input ->
    NCic.metasenv * NCic.substitution * 'status * NCic.term
 
 val disambiguate_nobj :
- #status as 'status ->
+ #LexiconTypes.status as 'status ->
  ?baseuri:string ->
  (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input ->
   'status * NCic.obj

diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml
index 9504e64ba377490d43bd7147637f5347c63b485a..fbcdccb31c3810604abb967e4492ca007514d345 100644 (file)
--- a/matita/components/ng_tactics/nTacStatus.ml
+++ b/matita/components/ng_tactics/nTacStatus.ml
@@ -66,7 +66,7 @@ class auto_status =
 
 class type g_pstatus =
  object
-  inherit GrafiteDisambiguate.g_status
+  inherit LexiconTypes.g_status
   inherit g_auto_status
   inherit g_eq_status
   method obj: NCic.obj
@@ -75,7 +75,7 @@ class type g_pstatus =
 class pstatus =
  fun (o: NCic.obj) ->
  object (self)
-   inherit GrafiteDisambiguate.status
+   inherit LexiconTypes.status
    inherit auto_status
    inherit eq_status
    val obj = o

diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli
index cfb7123bbf0453d90cad5ece72cb4e2d7a5629ff..ddaf9da80db58813f8355713e307c05efbbc3814 100644 (file)
--- a/matita/components/ng_tactics/nTacStatus.mli
+++ b/matita/components/ng_tactics/nTacStatus.mli
@@ -43,7 +43,7 @@ class auto_status :
 
 class type g_pstatus =
  object
-  inherit GrafiteDisambiguate.g_status
+  inherit LexiconTypes.g_status
   inherit g_auto_status
   inherit g_eq_status
   method obj: NCic.obj
@@ -52,7 +52,7 @@ class type g_pstatus =
 class pstatus :
  NCic.obj ->
   object ('self)
-   inherit GrafiteDisambiguate.status
+   inherit LexiconTypes.status
    inherit auto_status
    inherit eq_status
    method obj: NCic.obj

diff --git a/matita/components/statuses.txt b/matita/components/statuses.txt
index 104a909385b8be2a9346529e138c2dd0ead6bead..d4fb967b7be6c46b5acec12213c891abdcf48661 100644 (file)
--- a/matita/components/statuses.txt
+++ b/matita/components/statuses.txt
@@ -1,16 +1,20 @@
-grafitetypes -> tac -> auto + eq + (grafitedisambiguate = lexicon+nciccoercion)
-           |--> dumpable                                    |             |
-           |--> nciclibrary                                 |       unif_hint
-           |--> grafiteparser -> lexicon -> ...             |
-                                                            |-> interpretation
-                                                            |-> termcontentpres
-                                                            |-> notation_parser
-
+grafitetypes
+ |--> dumpable
+ |--> nciclibrary
+ |--> grafiteparser -----
+ |--> tac               |
+       |--> auto        |
+       |--> eq          |
+       |-------------> lexicon
+                        |--> notation_parser
+                        |--> interpretation
+                        |       |--> nciccoercion --> unif_hint
+                        |--> termcontentpres
 
 applytransformation
     |
-    |-> ntermciccontent = nciccoercion+interpretation
-    |                       |
-    |                    unif_hint
+    |-> interpretation -> nciccoercion
+    |                         |
+    |                     unif_hint
     |
     |-> termcontentpres