Ignore:
Timestamp:
Jul 24, 2012, 7:40:13 PM (8 years ago)
Author:
campbell
Message:

Tweak Cminor invariant to be slightly more readable/extendable.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2232 r2249  
    15821582     (* merge Hlabel_wf with Hstmt_inv and eliminate right away *)
    15831583     @(stmt_P_mp … (stmt_P_conj … Hstmt_inv Hlabel_wf))
    1584      #s * #Hstmt_vars #Hstmt_labels @conj
     1584     #s * #Hstmt_vars #Hstmt_labels %
    15851585     [ 1: (* prove that variables are either parameters or locals *)
    15861586        @(stmt_vars_mp … Hstmt_vars) #i #t #H
Note: See TracChangeset for help on using the changeset viewer.