Permalink
Browse files

don't include EquivDec because it overrides the notation <>

  • Loading branch information...
1 parent 3b52144 commit e22b4d7a1a78c4f2b40cb8f676c4107b1b6c9dd2 @gmalecha gmalecha committed May 20, 2013
Showing with 5 additions and 5 deletions.
  1. +4 −4 theories/Structures/EqDep.v
  2. +1 −1 tools/dir-locals.el
@@ -1,20 +1,20 @@
Require Coq.Logic.Eqdep_dec.
-Require Import EquivDec.
+Require EquivDec.
Set Implicit Arguments.
Set Strict Implicit.
Section Classes.
Context {A : Type}.
- Context {dec : EqDec A (@eq A)}.
+ Context {dec : EquivDec.EqDec A (@eq A)}.
Theorem UIP_refl : forall {x : A} (p1 : x = x), p1 = refl_equal _.
intros.
- eapply Coq.Logic.Eqdep_dec.UIP_dec. apply equiv_dec.
+ eapply Coq.Logic.Eqdep_dec.UIP_dec. apply EquivDec.equiv_dec.
Qed.
Theorem UIP_equal : forall {x y : A} (p1 p2 : x = y), p1 = p2.
- eapply Coq.Logic.Eqdep_dec.UIP_dec. apply equiv_dec.
+ eapply Coq.Logic.Eqdep_dec.UIP_dec. apply EquivDec.equiv_dec.
Qed.
Lemma inj_pair2 :
View
@@ -1,3 +1,3 @@
((coq-mode . ((coq-load-path . (
- (rec "PWD/theories" "ExtLib")
+ (nonrec "PWD/theories" "ExtLib")
)))))

0 comments on commit e22b4d7

Please sign in to comment.