X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fparamodulation%2Findexing.mli;h=d2807447c7000894106eb072ca8ca4b93697687c;hb=ed308fc03be5397081ac0e00bbc73b3f71da1e67;hp=9b051bc404b55f7bf58c5941b3e6ccce9ba88048;hpb=7562b71d0a7c232cd84018ed7e3d0e81a621d690;p=helm.git

diff --git a/helm/ocaml/tactics/paramodulation/indexing.mli b/helm/ocaml/tactics/paramodulation/indexing.mli
index 9b051bc40..d2807447c 100644
--- a/helm/ocaml/tactics/paramodulation/indexing.mli
+++ b/helm/ocaml/tactics/paramodulation/indexing.mli
@@ -83,6 +83,4 @@ val demodulation_theorem :
   Index.t ->
   Cic.term * Index.key * Cic.metasenv ->
   'a * (Cic.term * Index.key * Cic.metasenv)
-val demodulate_tac: 
-  dbd:HMysql.dbd ->  
-  pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
+