X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineTypes.mli;h=7c7b8330ee13d7cf075c6247dd4a293dc9520d16;hb=d0defade97cf8cf1b5426c73b16b7ea63ccaffbc;hp=6edcfeccc053a7559b715604e9a08f8c421a66f9;hpb=c6cc2a7227d6750076f591a62d7b1896ebf1ebfa;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineTypes.mli b/helm/software/components/tactics/proofEngineTypes.mli
index 6edcfeccc..7c7b8330e 100644
--- a/helm/software/components/tactics/proofEngineTypes.mli
+++ b/helm/software/components/tactics/proofEngineTypes.mli
@@ -75,3 +75,4 @@ type mk_fresh_name_type =
 
 val goals_of_proof: proof -> goal list
 
+val hole: Cic.term