Changeset 891 for src/Clight/Cexec.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/Clight/Cexec.ma

    r880 r891  
    344344] qed.
    345345
    346 definition is_Sskip : ∀s:statement. (s = Sskip) + (s ≠ Sskip) ≝
    347 λs.match s return λs'.(s' = Sskip) + (s' ≠ Sskip) with
     346definition is_Sskip : ∀s:statement. (s = Sskip) (s ≠ Sskip) ≝
     347λs.match s return λs'.(s' = Sskip) (s' ≠ Sskip) with
    348348[ Sskip ⇒ inl ?? (refl ??)
    349349| _ ⇒ inr ?? (nmk ? (λH.?))
Note: See TracChangeset for help on using the changeset viewer.