summaryrefslogtreecommitdiff
path: root/language/l2.lem
diff options
context:
space:
mode:
authorKathy Gray2015-08-06 16:24:28 +0100
committerKathy Gray2015-08-06 16:24:28 +0100
commitd4d2e262f96a8eef543c017c8df08c25f2715118 (patch)
treeb768f8818157caf1389d782d4f3070a2f80eab4d /language/l2.lem
parent43427019f9f2c1e64a07ec6ee3caef8bd1a5c165 (diff)
Update analysis to merge states and values after branches taken due to unknown conditions.
Does not merge if one path has resulted in an exit
Diffstat (limited to 'language/l2.lem')
-rw-r--r--language/l2.lem2
1 files changed, 1 insertions, 1 deletions
diff --git a/language/l2.lem b/language/l2.lem
index 7ee69d5e..63869068 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -544,7 +544,7 @@ type tag = (* Data indicating where the identifier arises and thus information
| Tag_spec
| Tag_enum of integer
| Tag_alias
- | Tag_unknown (* Tag to distinguish an unknown path from a non-analysis non deterministic path *)
+ | Tag_unknown of maybe string (* Tag to distinguish an unknown path from a non-analysis non deterministic path *)
type tinf = (* Type variables, type, and constraints, bound to an identifier *)