Changeset 1102 for Deliverables/D3.3/id-lookup-branch/Cminor/semantics.ma

Timestamp:

Aug 4, 2011, 1:55:53 PM (10 years ago)

Author:

campbell

Message:

Tidy up branch

File:

• Deliverables/D3.3/id-lookup-branch/Cminor/semantics.ma (modified) (2 diffs)

Deliverables/D3.3/id-lookup-branch/Cminor/semantics.ma

@@ -106 +106 @@
 ].
 
-let rec find_label (l:ident) (s:stmt) (k:cont) on s : option (stmt × cont) ≝
+let rec find_label (l:identifier Label) (s:stmt) (k:cont) on s : option (stmt × cont) ≝
 match s with
 [ St_seq s1 s2 ⇒
@@ -121 +121 @@
 | St_block s' ⇒ find_label l s' (Kblock k)
 | St_label l' s' ⇒ 
-    match ident_eq l l' with
+    match identifier_eq ? l l' with
     [ inl _ ⇒ Some ? 〈s',k〉
     | inr _ ⇒ find_label l s' k