From 016603891d57b4c6b41da6a398bf8ae466019f9e Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Mon, 14 Nov 2011 15:20:42 +0000 Subject: [PATCH] Bug fix in inversion: 1) Dependent inversion only makes sense for JMeq 2) Removed test line fixing is_dependent = true --- matita/components/ng_tactics/nInversion.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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 -- 2.39.2