Changeset 882 for src/RTLabs/import.ma


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

Fix up fragile proofs for current version of matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/import.ma

    r878 r882  
    6565  do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag);
    6666  let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in
    67   do graph ← foldr ?? (λp,g0. do g ← g0;
    68                               let 〈l,s〉 ≝ p in
    69                               do l' ← get_label l;
    70                               do s' ← s rmap get_label;
    71                               OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f);
     67  do graph ← foldr ?? (λp:nat × ((pre_register → res register) → (nat → res label) → res statement).λg0.
     68                         do g ← g0;
     69                         let 〈l,s〉 ≝ p in
     70                         do l' ← get_label l;
     71                         do s' ← s rmap get_label;
     72                         OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f);
    7273  do entry ← get_label (pf_entry pre_f);
    7374  do exit ← get_label (pf_exit pre_f);
Note: See TracChangeset for help on using the changeset viewer.