fixed defaultauto behaviour. not the cache is preserveed

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

diff --git a/helm/software/components/tactics/declarative.mli b/helm/software/components/tactics/declarative.mli
index e5a8a590c00b8687e62713ba9e4247e169c42f0e..3b02fb4d9c061c53a343998d433be16bab938aec 100644 (file)
--- 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