Bug fix in inversion:

1) Dependent inversion only makes sense for JMeq
2) Removed test line fixing is_dependent = true

diff --git a/matita/components/ng_tactics/nInversion.ml b/matita/components/ng_tactics/nInversion.ml
index dbbf0da0f4a17b225df93321cc8ffaf6230036a1..ee0cc41c3e68fb66eccd692a1bc03a486969f22f 100644 (file)
--- 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