X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmove_char.ma;h=297344d54140f180dc75d28f99d719ed073cf197;hb=39aab7babf51252cecb81a66af82fe797e8dcbe7;hp=e20591c5f607b725b2b6d4cd0a6038c3834c8fd2;hpb=fd282412fff8f2529bb1dfb22a684f5c25af37cb;p=helm.git

diff --git a/matita/matita/lib/turing/move_char.ma b/matita/matita/lib/turing/move_char.ma
index e20591c5f..297344d54 100644
--- a/matita/matita/lib/turing/move_char.ma
+++ b/matita/matita/lib/turing/move_char.ma
@@ -96,7 +96,7 @@ lemma sem_move_char_r :
 #alpha #sep #inc #i #outc #Hloop
 lapply (sem_while … (sem_mcr_step alpha sep) inc i outc Hloop) [%]
 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
-[ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
+[ whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
   %
   [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
     [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2)]
@@ -105,7 +105,7 @@ lapply (sem_while … (sem_mcr_step alpha sep) inc i outc Hloop) [%]
     [#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct %
     |*:% #H2 normalize in H2; destruct (H2) ]
   ]
-| #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
+| #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
   lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%); #IH
   #b0 #a0 #ls #rs #Htapea cases Hstar1 #b * #bsep *
   [* #a * #ls1 * #rs1 * >Htapea #H destruct (H) #Htapeb %
@@ -256,7 +256,7 @@ lemma sem_move_char_l :
 #alpha #sep #inc #i #outc #Hloop
 lapply (sem_while … (sem_mcl_step alpha sep) inc i outc Hloop) [%]
 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
-[ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
+[ whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
   %
   [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
     [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2)]
@@ -265,7 +265,7 @@ lapply (sem_while … (sem_mcl_step alpha sep) inc i outc Hloop) [%]
     [#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct %
     |*:% #H2 normalize in H2; destruct (H2) ]
   ]
-| #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
+| #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
   lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%); #IH
   #b0 #a0 #ls #rs #Htapea cases Hstar1 #b * #bsep *
   [* #a * #ls1 * #rs1 * >Htapea #H destruct (H) #Htapeb %