New version of the library. Several files still do not compile.

[helm.git] / matita / components / ng_tactics / nTacStatus.mli

diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli
index ddaf9da80db58813f8355713e307c05efbbc3814..30989faba8dcfeb6c96400cbe96bdc3932ae77fa 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 LexiconTypes.g_status
+  inherit GrafiteDisambiguate.g_status
   inherit g_auto_status
   inherit g_eq_status
   method obj: NCic.obj
@@ -52,10 +52,10 @@ class type g_pstatus =
 class pstatus :
  NCic.obj ->
   object ('self)
-   inherit LexiconTypes.status
+   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
@@ -107,7 +107,7 @@ val mk_meta:
  #pstatus as 'status -> ?attrs:NCic.meta_attrs -> NCic.context ->
    [ `Decl of cic_term | `Def of cic_term ] -> NCicUntrusted.meta_kind ->
      'status * cic_term
-val instantiate: #pstatus as 'status -> int -> cic_term -> 'status
+val instantiate: #pstatus as 'status -> ?refine:bool -> int -> cic_term -> 'status
 val instantiate_with_ast: #pstatus as 'status -> int -> tactic_term -> 'status
 
 val select_term:
@@ -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