]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/variousTactics.mli
renamed Http_client to Http_user_agent to avoid clashes with Gerd's
[helm.git] / helm / ocaml / tactics / variousTactics.mli
index c27e542ff1cbbe49513d7bb13532354b46c68223..ebbf843326b9d9f179b1e133ad6cb41528f9cbb4 100644 (file)
@@ -32,7 +32,6 @@ val generalize_tac:
  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term list ->
   ProofEngineTypes.tactic
 
-val auto_tac : 
- MQIConn.handle -> ProofEngineTypes.status ->
-   ProofEngineTypes.proof * ProofEngineTypes.goal list
+(* val auto_tac : MQIConn.handle -> ProofEngineTypes.tactic *)
+val auto_tac : dbh:Dbi.connection -> ProofEngineTypes.tactic