snapshot, notably:

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

diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml
index 54ebdf6cf7663340bf5907d433a63ee3f963854c..9afb90a714b36ca53090f0e63b68aa743d2bd9f0 100644 (file)
--- a/helm/matita/matitaProof.ml
+++ b/helm/matita/matitaProof.ml
@@ -151,4 +151,7 @@ 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