Moved paramodulation inside tactics.

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

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 25e479b4725197301f5fcafe11b73c25f3d41059..c8c225cddd2ae8a8015f8d3b241aecffa23c635b 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -23,6 +23,9 @@ val decompose :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?user_types:(UriManager.uri * int) list ->
   dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic
+val demodulate :
+  dbd:HMysql.dbd ->
+  pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 val discriminate : term:Cic.term -> ProofEngineTypes.tactic
 val elim_intros :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->