Bug fixed in injection: a missing lift bugged the tactic when the constructor

had more than one argument.
The tactic is still bugged when the inductive type has either right or left
parameters!

diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml
index 4c7f5148d1cb5a1ff225c676c7f4ea9931011b01..9c99989070feed492d555e8f1782e4a78f33faab 100644 (file)
--- a/helm/software/components/tactics/discriminationTactics.ml
+++ b/helm/software/components/tactics/discriminationTactics.ml
@@ -37,7 +37,8 @@ let rec injection_tac ~term =
   let _,metasenv,_,_ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let termty,_ = (* TASSI: FIXME *)
-    CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in  
+    CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
+  in
     ProofEngineTypes.apply_tactic
       (match termty with
           (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
@@ -59,7 +60,9 @@ let rec injection_tac ~term =
                             [],[] -> T.id_tac
                           | hd1::tl1,hd2::tl2 -> 
                              T.then_ 
-                              ~start:(injection1_tac ~i ~term)
+                              ~start:
+                                (injection1_tac ~i
+                                  ~term:(CicSubstitution.lift (i-1) term))
                               ~continuation:(traverse_list (i+1) tl1 tl2)
                           | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???"))
                        in traverse_list 1 applist1 applist2