X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnInversion.ml;h=ee0cc41c3e68fb66eccd692a1bc03a486969f22f;hb=dba584374a26ef04c53306c89e5567e637e6553e;hp=dbbf0da0f4a17b225df93321cc8ffaf6230036a1;hpb=085cf66f8385f8cbc269c38ca7c7572d09e4810e;p=helm.git

diff --git a/matita/components/ng_tactics/nInversion.ml b/matita/components/ng_tactics/nInversion.ml
index dbbf0da0f..ee0cc41c3 100644
--- a/matita/components/ng_tactics/nInversion.ml
+++ b/matita/components/ng_tactics/nInversion.ml
@@ -110,8 +110,7 @@ let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.st
  let nparams = List.length args in
 
  (* the default is a dependent inversion *)
- (*let is_dependent = selection = None in*)
- let is_dependent = true in
+ let is_dependent = (selection = None && jmeq) in
 
  pp (lazy ("nparams = " ^ string_of_int nparams));
  if nparams = 0