WARNING: partial commit (does not compile)

[helm.git] / matita / components / ng_cic_content / nTermCicContent.mli

diff --git a/matita/components/ng_cic_content/nTermCicContent.mli b/matita/components/ng_cic_content/nTermCicContent.mli
index d691acdec402bd11cc3f56f173dc47383065d2fc..f06ea2e91433c68036829339de42795592f03b13 100644 (file)
--- a/matita/components/ng_cic_content/nTermCicContent.mli
+++ b/matita/components/ng_cic_content/nTermCicContent.mli
@@ -87,13 +87,19 @@ type id = string
 
 val hide_coercions: bool ref
 
+class status :
+  object ('self)
+    inherit NCicCoercion.status
+    inherit Interpretations.status
+  end
+
 val nmap_sequent:
- #NCicCoercion.status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
+ #status as 'a -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
   int * NCic.conjecture ->
    NotationPt.term Content.conjecture *
     (id, NReference.reference) Hashtbl.t    (* id -> reference *)
 
 val nmap_obj:
- #NCicCoercion.status -> NCic.obj ->
+ #status -> NCic.obj ->
   NotationPt.term Content.cobj *
    (id, NReference.reference) Hashtbl.t    (* id -> reference *)