Minor code uniformization.

diff --git a/matita/components/grafite_parser/grafiteParser.mli b/matita/components/grafite_parser/grafiteParser.mli
index 451c17c68aa99b8e02d6e8b281aa2238f7aebe26..3e3f40e13183d3fbd10e8bcef2b2e3f8365adf9a 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.mli
+++ b/matita/components/grafite_parser/grafiteParser.mli
@@ -39,8 +39,8 @@ class type g_status =
 
 class status :
  object('self)
+  inherit g_status
   inherit CicNotationParser.status
-  method parser_db : db
   method set_parser_db : db -> 'self
   method set_parser_status : 'status. #g_status as 'status -> 'self
  end

diff --git a/matita/components/ng_cic_content/interpretations.mli b/matita/components/ng_cic_content/interpretations.mli
index 4b9fdae768c7e64385dbb71996535fce907a2795..2bf18caa6e24d2021933ecbcd9a537ecee632a75 100644 (file)
--- a/matita/components/ng_cic_content/interpretations.mli
+++ b/matita/components/ng_cic_content/interpretations.mli
@@ -38,8 +38,8 @@ class type g_status =
 
 class status :
   object ('self)
+    inherit g_status
     inherit NCicCoercion.status
-    method interp_db: db
     method set_interp_db: db -> 'self
     method set_interp_status: #g_status -> 'self
   end

diff --git a/matita/components/ng_refiner/nCicCoercion.mli b/matita/components/ng_refiner/nCicCoercion.mli
index f2cd526822b1f5342bf95fd1a27b307934a18c6e..d85484a2a4d02959f2451bea524972c56b5fc152 100644 (file)
--- a/matita/components/ng_refiner/nCicCoercion.mli
+++ b/matita/components/ng_refiner/nCicCoercion.mli
@@ -21,9 +21,8 @@ class type g_status =
 
 class status :
  object ('self)
-  inherit NCicUnifHint.status
   inherit g_status
-  method coerc_db: db
+  inherit NCicUnifHint.status
   method set_coerc_db: db -> 'self
   method set_coercion_status: #g_status -> 'self
  end

diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli
index cfb7123bbf0453d90cad5ece72cb4e2d7a5629ff..f9eb1917c3c243ba72574b1626bc415a464514f5 100644 (file)
--- a/matita/components/ng_tactics/nTacStatus.mli
+++ b/matita/components/ng_tactics/nTacStatus.mli
@@ -52,10 +52,10 @@ class type g_pstatus =
 class pstatus :
  NCic.obj ->
   object ('self)
+   inherit g_pstatus
    inherit GrafiteDisambiguate.status
    inherit auto_status
    inherit eq_status
-   method obj: NCic.obj
    method set_obj: NCic.obj -> 'self
    method set_pstatus: #g_pstatus -> 'self
   end
@@ -130,8 +130,8 @@ class type ['stack] g_status =
 class ['stack] status :
  NCic.obj -> 'stack ->
   object ('self)
+   inherit ['stack] g_status
    inherit pstatus
-   method stack: 'stack
    method set_stack: 'stack -> 'self
    method set_status: 'stack #g_status -> 'self
   end

diff --git a/matita/components/statuses.txt b/matita/components/statuses.txt
index 38800d6c016441d8c7d289df2792e583bc039be2..e6276014b23d8f772454f6755fc60c8a46978078 100644 (file)
--- a/matita/components/statuses.txt
+++ b/matita/components/statuses.txt
@@ -4,8 +4,7 @@ grafitetypes(baseuri,ng_mode)
  |--> grafiteparser(db=ast_statement grammarentry)
  |     |--> cicnotationparser(db=grammars+keywords+items)
  |
- |--> termcontentpres(db=level1_patterns21,compiled21,
- |                       pattern21_matrix,counter)
+ |--> termcontentpres(db=level1_patterns21,compiled21,pattern21_matrix,counter)
  |
  |--> tac(obj,stack)
        |--> auto(automation_cache)