From 29e65035d698f11ab4d3a627f8b9b6027f1f20d5 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 4 Nov 2010 22:42:11 +0000
Subject: [PATCH] Minor code uniformization.

---
 matita/components/grafite_parser/grafiteParser.mli   | 2 +-
 matita/components/ng_cic_content/interpretations.mli | 2 +-
 matita/components/ng_refiner/nCicCoercion.mli        | 3 +--
 matita/components/ng_tactics/nTacStatus.mli          | 4 ++--
 matita/components/statuses.txt                       | 3 +--
 5 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/matita/components/grafite_parser/grafiteParser.mli b/matita/components/grafite_parser/grafiteParser.mli
index 451c17c68..3e3f40e13 100644
--- 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 4b9fdae76..2bf18caa6 100644
--- 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 f2cd52682..d85484a2a 100644
--- 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 cfb7123bb..f9eb1917c 100644
--- 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 38800d6c0..e6276014b 100644
--- 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)
-- 
2.39.2