Mercurial > cpdt > repo
diff src/GeneralRec.v @ 426:5f25705a10ea
Pass through DataStruct, to incorporate new coqdoc features; globally replace [refl_equal] with [eq_refl]
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 25 Jul 2012 18:10:26 -0400 |
| parents | f83664d817ce |
| children | 8077352044b2 |
line wrap: on
line diff
--- a/src/GeneralRec.v Wed Jul 25 17:50:12 2012 -0400 +++ b/src/GeneralRec.v Wed Jul 25 18:10:26 2012 -0400 @@ -332,14 +332,14 @@ case_eq M; intros ? ? Heq; try rewrite Heq in *; subst | [ H : forall n v, ?E n = Some v -> _, _ : context[match ?E ?N with Some _ => _ | None => _ end] |- _ ] => - specialize (H N); destruct (E N); try rewrite (H _ (refl_equal _)) by auto; try discriminate + specialize (H N); destruct (E N); try rewrite (H _ (eq_refl _)) by auto; try discriminate | [ H : forall n v, ?E n = Some v -> _, H' : ?E _ = Some _ |- _ ] => rewrite (H _ _ H') by auto end; simpl in *); eauto 7. Ltac run := run'; repeat (match goal with | [ H : forall n v, ?E n = Some v -> _ |- context[match ?E ?N with Some _ => _ | None => _ end] ] => - specialize (H N); destruct (E N); try rewrite (H _ (refl_equal _)) by auto; try discriminate + specialize (H N); destruct (E N); try rewrite (H _ (eq_refl _)) by auto; try discriminate end; run'). Lemma ex_irrelevant : forall P : Prop, P -> exists n : nat, P. @@ -536,12 +536,12 @@ (* begin hide *) Lemma leq_Some : forall A (x y : A), leq (Some x) (Some y) -> x = y. - intros ? ? ? H; generalize (H _ (refl_equal _)); crush. + intros ? ? ? H; generalize (H _ (eq_refl _)); crush. Qed. Lemma leq_None : forall A (x y : A), leq (Some x) None -> False. - intros ? ? ? H; generalize (H _ (refl_equal _)); crush. + intros ? ? ? H; generalize (H _ (eq_refl _)); crush. Qed. Ltac mergeSort' := run;