Changeset 881 for src/common


Ignore:
Timestamp:
Jun 3, 2011, 5:35:31 PM (9 years ago)
Author:
campbell
Message:

Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/common/AST.ma

    r880 r881  
    479479  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
    480480Qed.
    481 *)
     481*)*)
    482482(* * * External functions *)
    483483
    … …  
    532532End TRANSF_PARTIAL_FUNDEF.
    533533*)
    534 *)
     534
    535535
    536536
Note: See TracChangeset for help on using the changeset viewer.