From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Fri, 4 Dec 2009 11:30:34 +0000 (+0000)
Subject: Bugfix in inversion (was using refl_eq instead of refl).
X-Git-Tag: make_still_working~3181
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=424d9c389cac763849bc10bd68cf3584d5d0ac02;p=helm.git

Bugfix in inversion (was using refl_eq instead of refl).
---

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