- changed license to lgpl

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

diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml
index 54ebdf6cf7663340bf5907d433a63ee3f963854c..99214e724d85cbd061f927e3c9f9f303ebaed866 100644 (file)
--- a/helm/matita/matitaProof.ml
+++ b/helm/matita/matitaProof.ml
@@ -151,4 +151,5 @@ let proof ?uri ~metasenv ~typ () =
   new proof ~typ ~metasenv ~body ?uri ()
 
 let currentProof () = new currentProof
+let instance = MatitaMisc.singleton currentProof