Mercurial > cpdt > repo

comparison src/Coinductive.v @ 88:cde1351d18bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Get Coinductive compiling again
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Oct 2008 10:43:54 -0400
parents f295a64bf9fd
children 32a5ad6e2bb0
comparison
equal deleted inserted replaced
87:a0b8b550e265 88:cde1351d18bb
410 (** We prove two lemmas about how register map modifications affect compatibility. A tactic [compat] abstracts the common structure of the two proofs. *) 410 (** We prove two lemmas about how register map modifications affect compatibility. A tactic [compat] abstracts the common structure of the two proofs. *)
411 411
412 (** remove printing * *) 412 (** remove printing * *)
413 Ltac compat := unfold regmapCompat in *; crush; 413 Ltac compat := unfold regmapCompat in *; crush;
414 match goal with 414 match goal with
415 | [ |- match get _ ?R with Some _ => _ | None => _ end ] => destruct R; crush 415 | [ H : _ |- match get _ ?R with Some _ => _ | None => _ end ] => generalize (H R); destruct R; crush
416 end. 416 end.
417 417
418 Lemma regmapCompat_set_None : forall rm rm' r n, 418 Lemma regmapCompat_set_None : forall rm rm' r n,
419 regmapCompat rm rm' 419 regmapCompat rm rm'
420 -> regmapCompat (set rm r n) (set rm' r None). 420 -> regmapCompat (set rm r n) (set rm' r None).