From 424d9c389cac763849bc10bd68cf3584d5d0ac02 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 4 Dec 2009 11:30:34 +0000 Subject: [PATCH] Bugfix in inversion (was using refl_eq instead of refl). --- helm/software/components/ng_tactics/nInversion.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml index 627885cb7..8df07952f 100644 --- a/helm/software/components/ng_tactics/nInversion.ml +++ b/helm/software/components/ng_tactics/nInversion.ml @@ -130,8 +130,8 @@ let mk_inverter name it leftno ?selection outsort status baseuri = mk_appl (mk_id "P"::id_rs))))) in let t = mk_appl ( [mk_id (ind_name ^ "_" ^ suffix)]@ id_ls @ [lambdas] @ - List.map mk_id hyplist @ - CicNotationPt.Implicit `Vector::[mk_id "Hterm"] ) in + List.map mk_id hyplist @ + HExtlib.mk_list (CicNotationPt.Implicit `JustOne) (List.length ys) @ [mk_id "Hterm"] ) in let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri (baseuri ^ name ^ ".def", 0,CicNotationPt.Theorem (`Theorem,name,theorem,Some @@ -158,7 +158,7 @@ let mk_inverter name it leftno ?selection outsort status baseuri = NTactics.branch_tac; NTactics.case_tac "end"; NTactics.apply_tac ("",0,mk_id "Hcut"); - NTactics.apply_tac ("",0,mk_id "refl_eq"); + NTactics.apply_tac ("",0,mk_id "refl"); NTactics.shift_tac; (*NTactics.case_tac "cut";*) NTactics.apply_tac ("",0,t); -- 2.39.2