snapshot, notably:

[helm.git] / helm / matita / matitaProof.ml

diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml
index 9afb90a714b36ca53090f0e63b68aa743d2bd9f0..99214e724d85cbd061f927e3c9f9f303ebaed866 100644 (file)
--- a/helm/matita/matitaProof.ml
+++ b/helm/matita/matitaProof.ml
@@ -151,7 +151,5 @@ let proof ?uri ~metasenv ~typ () =
   new proof ~typ ~metasenv ~body ?uri ()
 
 let currentProof () = new currentProof
-let instance =
-  let currentProof = lazy (currentProof ()) in 
-  fun () -> Lazy.force currentProof
+let instance = MatitaMisc.singleton currentProof