From 5e65f8d4e75d65df82d21a1a862de823d150a836 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 11 Oct 2007 08:44:09 +0000 Subject: [PATCH] Old inversion bug fixed: it used to work only on the last hypothesis (or sort of). --- components/tactics/inversion.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/components/tactics/inversion.ml b/components/tactics/inversion.ml index 19d0c739a..e61021244 100644 --- a/components/tactics/inversion.ml +++ b/components/tactics/inversion.ml @@ -336,8 +336,8 @@ let inversion_tac ~term = for n = 1 to arity_consno do a := (Cic.Implicit None)::(!a) done; - (* apply i_inv ? ...? H). *) - Cic.Appl ([Cic.Const(uri,[])] @ !a @ [Cic.Rel 1]) + (* apply i_inv ? ...? H). *) + Cic.Appl ([Cic.Const(uri,[])] @ !a @ [term]) in let t = appl_term (arity_length + (List.length cons_list)) inversor_uri in let (t1,metasenv,_subst,t3,t4, attrs) = proof in -- 2.39.2