Changeset 882 for src/RTLabs/import.ma

Timestamp:

Jun 3, 2011, 5:35:32 PM (9 years ago)

Author:

campbell

Message:

Fix up fragile proofs for current version of matita.

File:

• src/RTLabs/import.ma (modified) (1 diff)

src/RTLabs/import.ma

@@ -65 +65 @@
   do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag);
   let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in
-  do graph ← foldr ?? (λp,g0. do g ← g0;
-                              let 〈l,s〉 ≝ p in
-                              do l' ← get_label l;
-                              do s' ← s rmap get_label;
-                              OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f);
+  do graph ← foldr ?? (λp:nat × ((pre_register → res register) → (nat → res label) → res statement).λg0.
+                         do g ← g0;
+                         let 〈l,s〉 ≝ p in
+                         do l' ← get_label l;
+                         do s' ← s rmap get_label;
+                         OK ? (add ?? g l' s')) (OK ? (empty_map ??)) (pf_graph pre_f);
   do entry ← get_label (pf_entry pre_f);
   do exit ← get_label (pf_exit pre_f);