From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Mon, 14 Nov 2011 15:20:42 +0000 (+0000)
Subject: Bug fix in inversion:
X-Git-Tag: make_still_working~2117
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=016603891d57b4c6b41da6a398bf8ae466019f9e;p=helm.git

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 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