diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2011-08-06 13:07:50 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2011-08-06 13:07:50 -0400 |
| commit | f8d463b31a6808a1b83fa5873f295006b73daf72 (patch) | |
| tree | 2be2fc0cdd9c0f77ff56629d2cb576bf6e12f467 | |
| parent | 64f43be321e5ad4bef303831a589e1bd415e8673 (diff) | |
Better wildification, avoiding some unintentional variable capture
| -rw-r--r-- | src/elaborate.sml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index c043ef54..1b8a7dbe 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1,4 +1,4 @@ -(* Copyright (c) 2008-2010, Adam Chlipala +(* Copyright (c) 2008-2011, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -3380,8 +3380,12 @@ and wildifyStr env (str, sgn) = | L'.KRel _ => NONE | L'.KFun _ => NONE - fun decompileCon env (c, loc) = - case c of + fun maybeHnorm env c = + hnormCon env c + handle E.UnboundNamed _ => c + + fun decompileCon env (c as (_, loc)) = + case #1 (maybeHnorm env c) of L'.CRel i => let val (s, _) = E.lookupCRel env i |