Updated the _CoqProject file to reflect the new target file name. Mar…

…ked the Forall_tail and Exists_impl functions as local because I eventually plan to have these addded to the Standard Library and do not want naming conflics.
llee454 · Aug 24, 2018 · bfcc4f5 · bfcc4f5
1 parent 7460c06
commit bfcc4f5
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -1,3 +1,3 @@
--R . pigeons
+-R . pigeonhole_principle
 ./base.v
-./pigeons.v
+./pigeonhole_principle.v
diff --git a/pigeonhole_principle.v b/pigeonhole_principle.v
@@ -98,7 +98,7 @@ Definition containers_ok (cs : containers) : Prop
   element in [x0 :: xs], then [P] is true for
   every element in [xs].
 *)
-Definition Forall_tail
+Local Definition Forall_tail
   :  forall (A : Type) (P : A -> Prop) (x0 : A) (xs : list A), Forall P (x0 :: xs) -> Forall P xs
   := fun _ P x0 xs H
        => let H0
@@ -119,7 +119,7 @@ Arguments Forall_tail {A} {P} x0 xs.
   [P] is true, then there exists an element in
   [xs] for which [Q] is true.
 *)
-Definition Exists_impl
+Local Definition Exists_impl
   :  forall (A : Type) (P Q : A -> Prop),
      (forall x : A, P x -> Q x) ->
      forall xs : list A,