Ignore:
Timestamp:
Nov 19, 2012, 5:13:21 PM (7 years ago)
Author:
campbell
Message:

Get compiler.ma and correctness.ma checking again. Note that the back-end
is in a state of flux at the moment, so is axiomatised out.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r2395 r2475  
    319319    [ %{v} @Efd
    320320    | cases v in Efd;
    321       [ 5: * #b #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd;
     321      [ 4: * #b #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd;
    322322           [ #E @E | #E normalize in E; destruct ]
    323323      | *: normalize #A try #B try #C destruct
Note: See TracChangeset for help on using the changeset viewer.