Ignore:
Timestamp:
Dec 14, 2011, 3:35:41 PM (8 years ago)
Author:
sacerdot
Message:

All of Cminor now compiles with the latest lib of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r1605 r1611  
    634634| 9,10: #l #H @(present_included … H) repeat @fn_includes_step @I
    635635| @(pi2 ?? (pf_entry ??))
    636 | @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (pi2 ? (add_stmt_inv ???) ?)) ]
     636| @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added … (pi2 … f)) ]
    637637| % [ @pi2 | @(pi2 ?? exits) ]
    638 | @(equal_Cminor_labels_added ?? s) [ @refl | (*XXX@(stmt_labels_added ???? (pi2 ? (add_stmt_inv ???) ?))*) ]
    639 | #l #H cut (∀A,P. ∀c: Σx:A.P x. P (pi1 … c)) [2: #pi2' @(pi2' ? (λx.present ????) ?)
     638| @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added … (pi2 … f)) ]
     639| #l' #H @(pi2 ?? l)
    640640| #l #H @(present_included … (pi2 ?? l_default)) repeat @fn_includes_step @I
    641641| #l #H % [ @(present_included … (pi2 ?? l_case)) repeat @fn_includes_step @I | @H ]
    642 | @pi2
     642| @(pi2 … (pf_entry …))
    643643| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
    644         |@Cminor_labels_sig @(stmt_labels_added ???? (pi2 ? (add_stmt_inv ???) ?))
     644        |@Cminor_labels_sig @(stmt_labels_added … (pi2 … f))
    645645        ]
    646646| #l1 #H whd %2 @lookup_label_lpresent
    647 | @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ? (add_stmt_inv ???) ?)) ]
     647| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added … (pi2 … f)) ]
    648648] qed.
    649649
Note: See TracChangeset for help on using the changeset viewer.