Changeset 891 for src/common/Mem.ma


Ignore:
Timestamp:
Jun 7, 2011, 4:53:53 PM (9 years ago)
Author:
campbell
Message:

Revise proofs affected by recent matita change.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Mem.ma

    r790 r891  
    6666  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A.
    6767  update_block … x v f x = v.
    68 #A * * #ix #v #f whd in ⊢ (??%?);
    69 >(eqZb_z_z …) //;
     68#A * * #ix #v #f whd in ⊢ (??%?)
     69>eq_block_b_b //
    7070qed.
    7171
Note: See TracChangeset for help on using the changeset viewer.