X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FproofEngineTypes.mli;h=6edcfeccc053a7559b715604e9a08f8c421a66f9;hb=b8f54b66890a55cfc255fa1df3e40fe60b78ee15;hp=f326a469f126cb65e376b66947c86280520d6bcb;hpb=e00d05ab58597620345c2fd49b84a23efa8db34c;p=helm.git

diff --git a/components/tactics/proofEngineTypes.mli b/components/tactics/proofEngineTypes.mli
index f326a469f..6edcfeccc 100644
--- a/components/tactics/proofEngineTypes.mli
+++ b/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 * Cic.term * Cic.attribute list
   (** current goal, integer index *)
 type goal = int
 type status = proof * goal