X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fdeclarative.mli;h=3b02fb4d9c061c53a343998d433be16bab938aec;hb=004ccf29097c8ab5c4997555b54aba5831fa035a;hp=e5a8a590c00b8687e62713ba9e4247e169c42f0e;hpb=d348c454be6bae89169ed2948067e62e33f62bd8;p=helm.git

diff --git a/helm/software/components/tactics/declarative.mli b/helm/software/components/tactics/declarative.mli
index e5a8a590c..3b02fb4d9 100644
--- a/helm/software/components/tactics/declarative.mli
+++ b/helm/software/components/tactics/declarative.mli
@@ -28,13 +28,13 @@ val assume : string -> Cic.term -> ProofEngineTypes.tactic
 val suppose : Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic
 
 val by_term_we_proved :
- dbd:HMysql.dbd -> Cic.term option -> Cic.term -> string -> Cic.term option ->
+ dbd:HMysql.dbd -> Cic.term option -> Cic.term -> string option -> Cic.term option ->
   ProofEngineTypes.tactic
 
 val bydone : dbd:HMysql.dbd -> Cic.term option -> ProofEngineTypes.tactic
 
 val we_need_to_prove :
- Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic
+ Cic.term -> string option -> Cic.term option -> ProofEngineTypes.tactic
 
 val we_proceed_by_induction_on : Cic.term -> Cic.term -> ProofEngineTypes.tactic