Changeset 1082 for src/common

Timestamp:

Jul 20, 2011, 5:17:38 PM (10 years ago)

Author:

mulligan

Message:

work from today on ertl -> ltl pass

File:

• src/common/Graphs.ma (modified) (1 diff)

src/common/Graphs.ma

@@ -3 +3 @@
 include "ASM/BitVectorTrie.ma".
 include "common/Identifiers.ma".
+include "common/AST.ma".
 
 axiom LabelTag : String.
 
 definition label ≝ identifier LabelTag.
+
+(* o'caml compiler doesn't make distinction between idents and labels *)
+definition label_to_ident: label → ident ≝
+  λl.
+  match l with
+  [ an_identifier l ⇒ an_identifier SymbolTag l
+  ].
 
 definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?.