X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnInversion.mli;h=b5ca8597d9b53f0f13bf0875c22b912c86034c07;hb=711a06aebcd4f8e1127a56d82dd1fc4de22d5ea2;hp=4d6de91ed5898333be4871098700353dd7cd2944;hpb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;p=helm.git

diff --git a/helm/software/components/ng_tactics/nInversion.mli b/helm/software/components/ng_tactics/nInversion.mli
index 4d6de91ed..b5ca8597d 100644
--- a/helm/software/components/ng_tactics/nInversion.mli
+++ b/helm/software/components/ng_tactics/nInversion.mli
@@ -11,5 +11,6 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-val mk_inverter: string -> NCic.inductiveType -> int -> (#NTacStatus.tac_status as 's) -> string -> 's * NCic.obj
-
+val mk_inverter: string -> NCic.inductiveType -> int -> ?selection:bool list ->
+  NCic.sort -> (#NTacStatus.tac_status as 's) -> string -> 
+  's * NCic.obj