Mercurial > urweb
comparison src/elab_ops.sml @ 328:58f1260f293f
Fixed a mind-numbing De Bruijn bug
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 11 Sep 2008 19:59:31 -0400 |
parents | 950320f33232 |
children | eec65c11d3e2 |
comparison
equal
deleted
inserted
replaced
327:3a57f3b3a3f8 | 328:58f1260f293f |
---|---|
90 let | 90 let |
91 val sc = (hnormCon env (subConInCon (0, c2) cb)) | 91 val sc = (hnormCon env (subConInCon (0, c2) cb)) |
92 handle SynUnif => cAll | 92 handle SynUnif => cAll |
93 (*val env' = E.pushCRel env x k*) | 93 (*val env' = E.pushCRel env x k*) |
94 in | 94 in |
95 (*eprefaces "Subst" [("x", Print.PD.string x), | 95 (*Print.eprefaces "Subst" [("x", Print.PD.string x), |
96 ("cb", p_con env' cb), | 96 ("cb", ElabPrint.p_con env' cb), |
97 ("c2", p_con env c2), | 97 ("c2", ElabPrint.p_con env c2), |
98 ("sc", p_con env sc)];*) | 98 ("sc", ElabPrint.p_con env sc)];*) |
99 sc | 99 sc |
100 end | 100 end |
101 | c1' as CApp (c', i) => | 101 | c1' as CApp (c', i) => |
102 let | 102 let |
103 fun default () = (CApp ((c1', loc), hnormCon env c2), loc) | 103 fun default () = (CApp ((c1', loc), hnormCon env c2), loc) |