Mercurial > urweb

diff src/elaborate.sml @ 1529:a8a538800278

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Better wildification, avoiding some unintentional variable capture
author Adam Chlipala <adam@chlipala.net>
date Sat, 06 Aug 2011 13:07:50 -0400
parents cccf8bf64b30
children 7efcf8f4a44a
line wrap: on
line diff
--- a/src/elaborate.sml	Thu Aug 04 17:06:50 2011 -0400
+++ b/src/elaborate.sml	Sat Aug 06 13:07:50 2011 -0400
@@ -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 @@
                        | 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