From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 13 Sep 2006 12:53:01 +0000 (+0000)
Subject: Bug fixed in injection: a missing lift bugged the tactic when the constructor
X-Git-Tag: 0.4.95@7852~1043
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=407e4f0b8f189b38fcffd6438afce4bc4aa83f01;p=helm.git

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/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml
index 4c7f5148d..9c9998907 100644
--- a/components/tactics/discriminationTactics.ml
+++ b/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