Code restructuring.

[helm.git] / helm / ocaml / tactics / paramodulation / indexing.mli

diff --git a/helm/ocaml/tactics/paramodulation/indexing.mli b/helm/ocaml/tactics/paramodulation/indexing.mli
index 9b051bc404b55f7bf58c5941b3e6ccce9ba88048..d2807447c7000894106eb072ca8ca4b93697687c 100644 (file)
--- 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
+