X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ftactics.mli;h=c8c225cddd2ae8a8015f8d3b241aecffa23c635b;hb=cbac948d507d74a558ba7f11ce10bc252b1ba8ba;hp=25e479b4725197301f5fcafe11b73c25f3d41059;hpb=827e35d6058ebba3a4a4fa6eb3c160f0cd0fd1e8;p=helm.git

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 25e479b47..c8c225cdd 100644
--- 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 ->