comparison src/disjoint.sml @ 345:b85e6ba56618

Merge CDisjoint and TDisjoint
author Adam Chlipala <adamc@hcoop.net>
date Sat, 04 Oct 2008 15:50:28 -0400
parents bc5015b89dd2
children 6ee1c761818f
comparison
equal deleted inserted replaced
344:3c0feecd057d 345:b85e6ba56618
313 in 313 in
314 (c, prove env denv (c1, c2, loc) @ gs) 314 (c, prove env denv (c1, c2, loc) @ gs)
315 end 315 end
316 in 316 in
317 case c of 317 case c of
318 CDisjoint cs => doDisj cs 318 CDisjoint (Instantiate, c1, c2, c) => doDisj (c1, c2, c)
319 | TDisjoint (Instantiate, c1, c2, c) => doDisj (c1, c2, c)
320 | _ => (cAll, []) 319 | _ => (cAll, [])
321 end 320 end
322 321
323 end 322 end