X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaProof.mli;h=9ed6221917d215277b6783435b788bb4ebeb51b9;hb=7deafec4fd4b2eebf4d4061f21ee5c47bd15b062;hp=566777fc1c8e3e61135127b1c1014a1e33f162e6;hpb=51971de8dfcf257680cf38f01f9bf53d9912a498;p=helm.git

diff --git a/helm/matita/matitaProof.mli b/helm/matita/matitaProof.mli
index 566777fc1..9ed622191 100644
--- a/helm/matita/matitaProof.mli
+++ b/helm/matita/matitaProof.mli
@@ -36,7 +36,7 @@ val proof:
     MatitaTypes.proof
 
   (** current proof handler *)
-class currentProof:
+class type currentProof =
   object
     inherit MatitaTypes.currentProof
     
@@ -52,3 +52,8 @@ class currentProof:
     method connect: [`Abort|`Quit] -> (unit -> bool) -> unit
   end
 
+val currentProof: unit -> currentProof
+
+  (** currentProof singleton instance *)
+val instance: unit -> currentProof
+