X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FproofEngineTypes.mli;h=7c7b8330ee13d7cf075c6247dd4a293dc9520d16;hb=249d11773d32add20d665c4f8521b7380e4fec0a;hp=4396ea78f62879e678faa487127f750afbb21699;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/tactics/proofEngineTypes.mli b/components/tactics/proofEngineTypes.mli
index 4396ea78f..7c7b8330e 100644
--- a/components/tactics/proofEngineTypes.mli
+++ b/components/tactics/proofEngineTypes.mli
@@ -26,7 +26,8 @@
   (**
     current proof (proof uri * metas * (in)complete proof * term to be prooved)
   *)
-type proof = UriManager.uri option * Cic.metasenv * Cic.term * Cic.term
+type proof =
+ 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
@@ -34,7 +35,7 @@ type status = proof * goal
   (** @param goal
   * @param goal's metasenv
   * @return initial proof status for the given goal *)
-val initial_status: Cic.term -> Cic.metasenv -> status
+val initial_status: Cic.term -> Cic.metasenv -> Cic.attribute list -> status
 
   (**
     a tactic: make a transition from one status to another one or, usually,
@@ -74,3 +75,4 @@ type mk_fresh_name_type =
 
 val goals_of_proof: proof -> goal list
 
+val hole: Cic.term