X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnInversion.mli;h=14d33eb1ee1be16fa9442439329ad76a14208084;hb=a77d0bd6a04e94f765d329d47b37d9e04d349b14;hp=b5ca8597d9b53f0f13bf0875c22b912c86034c07;hpb=da5dd88bbcc43d9f4342e47c922b820abf91c92f;p=helm.git diff --git a/helm/software/components/ng_tactics/nInversion.mli b/helm/software/components/ng_tactics/nInversion.mli index b5ca8597d..14d33eb1e 100644 --- a/helm/software/components/ng_tactics/nInversion.mli +++ b/helm/software/components/ng_tactics/nInversion.mli @@ -11,6 +11,7 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -val mk_inverter: string -> NCic.inductiveType -> int -> ?selection:bool list -> +val mk_inverter: + string -> bool -> NCic.inductiveType -> int -> ?selection:bool list -> NCic.sort -> (#NTacStatus.tac_status as 's) -> string -> - 's * NCic.obj + 's * NCic.obj