X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FeliminationTactics.mli;h=b203bee22947c7aa94e6ca376295a1f61f41f187;hb=b637879a2b3f2ceda65afb3c950061189c4730b7;hp=492566042911d1bdc71a7e3eb115f90bc376c90a;hpb=cea3a50f515d1e39467073d2b447a9ddfa1a4852;p=helm.git

diff --git a/helm/software/components/tactics/eliminationTactics.mli b/helm/software/components/tactics/eliminationTactics.mli
index 492566042..b203bee22 100644
--- a/helm/software/components/tactics/eliminationTactics.mli
+++ b/helm/software/components/tactics/eliminationTactics.mli
@@ -28,5 +28,6 @@ val elim_type_tac:
   ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
 
 val decompose_tac:
+ ?sorts:string list ->
  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
  unit -> ProofEngineTypes.tactic