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)