apply_subst_context on statuses

[helm.git] / helm / software / components / ng_tactics / nInversion.mli

diff --git a/helm/software/components/ng_tactics/nInversion.mli b/helm/software/components/ng_tactics/nInversion.mli
index 4d6de91ed5898333be4871098700353dd7cd2944..14d33eb1ee1be16fa9442439329ad76a14208084 100644 (file)
--- a/helm/software/components/ng_tactics/nInversion.mli
+++ b/helm/software/components/ng_tactics/nInversion.mli
@@ -11,5 +11,7 @@
 
 (* $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 -> bool -> NCic.inductiveType -> int -> ?selection:bool list ->
+  NCic.sort -> (#NTacStatus.tac_status as 's) -> string -> 
+   's * NCic.obj