]> matita.cs.unibo.it Git - helm.git/commitdiff
Cleared unused variables in wsem_match (they were also sharing names with
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Thu, 6 Dec 2012 15:40:58 +0000 (15:40 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Thu, 6 Dec 2012 15:40:58 +0000 (15:40 +0000)
other variables).

matita/matita/lib/turing/multi_universal/match.ma

index 9df8257fa7e443b44fd0875a789107a2c0d40b24..9c489372766309f5c4934bbd8eba1760dced2918 100644 (file)
@@ -401,7 +401,7 @@ lapply (sem_while … (sem_match_step src dst sig n is_startc is_endc Hneq Hsrc
      >reverse_cons >associative_append @(HFalse ?? Hnotnil)
     ]
   ]
-|#ta #tb #tc #Htrue #Hstar #IH #Hout lapply (IH Hout) -IH -Hout #IH whd
+|-ta -tb #ta #tb #tc #Htrue #Hstar #IH #Hout lapply (IH Hout) -IH -Hout #IH whd
  #ls #x #xs #end #rs #Hmid_src #Hnotend #Hend #Hnotstart 
  lapply (refl ? (current ? (nth dst ? ta (niltape ?))))
  cases (current ? (nth dst ? ta (niltape ?))) in ⊢ (???%→?);