Mercurial > cpdt > repo

comparison src/Coinductive.v @ 65:21bb59c56b98

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove [done] markers after enhancement phase finishes
author Adam Chlipala <adamc@hcoop.net>
date Wed, 01 Oct 2008 09:32:36 -0400
parents 739c2818d6e2
children 55199444e5e7
comparison
equal deleted inserted replaced
64:739c2818d6e2 65:21bb59c56b98
411 -> forall rm', regmapCompat rm rm' 411 -> forall rm', regmapCompat rm rm'
412 -> run prog rm (constFold rm' is) v. 412 -> run prog rm (constFold rm' is) v.
413 Hint Resolve regmapCompat_set_None regmapCompat_set_Some. 413 Hint Resolve regmapCompat_set_None regmapCompat_set_Some.
414 Hint Constructors run. 414 Hint Constructors run.
415 415
416 cofix. 416 cofix;
417 destruct 1; crush; eauto; 417 destruct 1; crush; eauto;
418 repeat match goal with 418 repeat match goal with
419 | [ H : regmapCompat _ _ |- run _ _ (match get ?RM ?R with Some _ => _ | None => _ end) _ ] => 419 | [ H : regmapCompat _ _ |- run _ _ (match get ?RM ?R with Some _ => _ | None => _ end) _ ] =>
420 generalize (H R); destruct (get RM R); crush 420 generalize (H R); destruct (get RM R); crush
421 end. 421 end.
422 Qed. 422 Qed.
423 End constFold_ok. 423 End constFold_ok.
424 424
425 Print constFold_ok. 425 Print constFold_ok.