Mercurial > cpdt > repo

comparison src/DataStruct.v @ 417:539ed97750bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update for Coq trunk version intended for final 8.4 release
author Adam Chlipala <adam@chlipala.net>
date Tue, 17 Jul 2012 16:37:58 -0400
parents fc03a67810e8
children 5f25705a10ea
comparison
equal deleted inserted replaced
416:ded318830bb0 417:539ed97750bb
771 match e with 771 match e with
772 | NConst n => NConst n 772 | NConst n => NConst n
773 | Plus e1 e2 => 773 | Plus e1 e2 =>
774 let e1' := cfold e1 in 774 let e1' := cfold e1 in
775 let e2' := cfold e2 in 775 let e2' := cfold e2 in
776 match e1', e2' return _ with 776 match e1', e2' return exp' Nat with
777 | NConst n1, NConst n2 => NConst (n1 + n2) 777 | NConst n1, NConst n2 => NConst (n1 + n2)
778 | _, _ => Plus e1' e2' 778 | _, _ => Plus e1' e2'
779 end 779 end
780 | Eq e1 e2 => 780 | Eq e1 e2 =>
781 let e1' := cfold e1 in 781 let e1' := cfold e1 in
782 let e2' := cfold e2 in 782 let e2' := cfold e2 in
783 match e1', e2' return _ with 783 match e1', e2' return exp' Bool with
784 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false) 784 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
785 | _, _ => Eq e1' e2' 785 | _, _ => Eq e1' e2'
786 end 786 end
787 787
788 | BConst b => BConst b 788 | BConst b => BConst b