X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineTypes.mli;h=7e6f571e42387c63902fba2db884c8ebc31ceeaa;hb=4ccc7ef7fe3d43fb0f882768d2818a54e24c8857;hp=f326a469f126cb65e376b66947c86280520d6bcb;hpb=61a2faa2694907757dd617175e0144705e79d65a;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineTypes.mli b/helm/software/components/tactics/proofEngineTypes.mli
index f326a469f..7e6f571e4 100644
--- a/helm/software/components/tactics/proofEngineTypes.mli
+++ b/helm/software/components/tactics/proofEngineTypes.mli
@@ -27,7 +27,7 @@
     current proof (proof uri * metas * (in)complete proof * term to be prooved)
   *)
 type proof =
- UriManager.uri option * Cic.metasenv * Cic.term * Cic.term * Cic.attribute list
+ UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term Lazy.t * Cic.term * Cic.attribute list
   (** current goal, integer index *)
 type goal = int
 type status = proof * goal
@@ -75,3 +75,4 @@ type mk_fresh_name_type =
 
 val goals_of_proof: proof -> goal list
 
+val hole: Cic.term