Ignore:
Timestamp:
Oct 10, 2011, 5:16:11 PM (8 years ago)
Author:
sacerdot
Message:

The new auto is much more powerful.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r1336 r1342  
    471471    | @step_for_start //;
    472472    ]
     473  | whd in ⊢ (?????%); cases k; // #k' @step_skip_break_switch %2 //
    473474  | whd in ⊢ (?????%); cases k; //;
    474     [ #s' #k' whd (* XXX // *) @step_break_seq
    475     | #ex #s' #k' whd (* //; *) @step_break_while
    476     | #ex #s' #k' whd (* //; *) @step_break_dowhile
    477     | #ex #s1 #s2 #k' whd (* //; *) @step_break_for2
    478     | #k' @step_skip_break_switch %2  //
    479     ]
    480   | whd in ⊢ (?????%); cases k; //;
    481     [ #s' #k' whd; (* XXX //;*) @step_continue_seq
    482     | #ex #s' #k' whd; @step_skip_or_continue_while %2 ; //;
     475    [ #ex #s' #k' whd; @step_skip_or_continue_while %2 ; //;
    483476    | #ex #s' #k' whd;
    484477      @res_bindIO2_OK #v #tr #Hv
     
    492485      ]
    493486    | #ex #s1 #s2 #k' whd; @step_skip_or_continue_for2 %2 ; //
    494     | #k' whd; (* XXX //;*) @step_continue_switch
    495487    ]
    496488  | #r whd in ⊢ (?????%); cases r;
Note: See TracChangeset for help on using the changeset viewer.