parameter sintax added to axiom statement

[helm.git] / helm / software / components / tactics / proofEngineTypes.mli

diff --git a/helm/software/components/tactics/proofEngineTypes.mli b/helm/software/components/tactics/proofEngineTypes.mli
index 7c7b8330ee13d7cf075c6247dd4a293dc9520d16..7e6f571e42387c63902fba2db884c8ebc31ceeaa 100644 (file)
--- 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.substitution * 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