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;