aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/disjoint.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-09-13 19:53:07 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-09-13 19:53:07 -0400
commit291fe704e9a5be0a71cd03418ec5229c99910898 (patch)
treee1698a7232fbee02d36d8a826948544a35420c1f /src/disjoint.sml
parent92865c5cf94bde77b7250450042e915a48e0025d (diff)
Name disjointness check changed to case insensitive
Diffstat (limited to 'src/disjoint.sml')
-rw-r--r--src/disjoint.sml4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/disjoint.sml b/src/disjoint.sml
index 8dff81e7..f3a98b51 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -143,9 +143,11 @@ fun enter denv =
PM.insert (denv', pieceEnter p, PS.map pieceEnter pset))
PM.empty denv
+val lowercase = CharVector.map Char.toLower
+
fun prove1 denv (p1, p2) =
case (p1, p2) of
- ((NameC s1, _), (NameC s2, _)) => s1 <> s2
+ ((NameC s1, _), (NameC s2, _)) => lowercase s1 <> lowercase s2
| _ =>
case PM.find (denv, p1) of
NONE => false