Merge pull request #7 from anlun/opam

OPAM support
vafeiadis · Sep 11, 2018 · ce18685 · ce18685
2 parents 0773f2a + e44b33d
commit ce18685
Show file tree

Hide file tree

Showing 5 changed files with 23 additions and 6 deletions.
diff --git a/HahnRewrite.v b/HahnRewrite.v
@@ -553,7 +553,7 @@ Tactic Notation "unfolder_prepare"  "in" hyp(H) :=
   repeat hahn_rewrite <- id_union in H.
 
 Tactic Notation "unfolder" := 
-  unfolder_prepare; autounfold with unfolderDb.
+  unfolder_prepare; repeat autounfold with unfolderDb.
 
 Tactic Notation "unfolder" "in" hyp(H) := 
   unfolder_prepare in H; autounfold with unfolderDb in H.

diff --git a/HahnSets.v b/HahnSets.v
@@ -75,7 +75,8 @@ Hint Unfold set_collect set_bunion set_disjoint : unfolderDb.
 
 Section SetProperties.
   Local Ltac u :=
-    autounfold with unfolderDb in *; ins; try solve [tauto | firstorder | split; ins; tauto].
+    repeat autounfold with unfolderDb in *;
+    ins; try solve [tauto | firstorder | split; ins; tauto].
 
   Variables A B C : Type.
   Implicit Type a : A.
@@ -523,15 +524,15 @@ Lemma set_finite_coinfinite_nat (s: nat -> Prop) :
 Proof.
   assert (LT: forall l x, In x l -> x <= fold_right Init.Nat.add 0 l).
     induction l; ins; desf; try apply IHl in H; omega.
-  autounfold with unfolderDb; red; ins; desf. 
+  repeat autounfold with unfolderDb; red; ins; desf. 
   tertium_non_datur (s (S (fold_right plus 0 findom + fold_right plus 0 findom0))) as [X|X];
    [apply H in X | apply H0 in X]; apply LT in X; omega.
 Qed.
 
 Lemma set_coinfinite_fresh (s: nat -> Prop) (COINF: set_coinfinite s) :
   exists b, ~ s b /\ set_coinfinite (s ∪₁ eq b).
 Proof.
-  autounfold with unfolderDb in *.
+  repeat autounfold with unfolderDb in *.
   tertium_non_datur (forall b, s b).
     by destruct COINF; exists nil; ins; desf.
   exists n; splits; red; ins; desf.
@@ -587,7 +588,7 @@ Proof. autounfold with unfolderDb; ins; desf; eauto. Qed.
 
 Add Parametric Morphism A B : (@set_collect A B) with signature 
   eq ==> set_equiv ==> set_equiv as set_collect_more.
-Proof. autounfold with unfolderDb; splits; ins; desf; eauto. Qed.
+Proof. repeat autounfold with unfolderDb; splits; ins; desf; eauto. Qed.
 
 Add Parametric Morphism A : (@set_disjoint A) with signature 
   set_subset --> set_subset --> Basics.impl as set_disjoint_mori.

diff --git a/_CoqProject b/_CoqProject
@@ -1,4 +1,4 @@
--R . Top
+-R . hahn 
 Hahn.v 
 HahnBase.v HahnFun.v HahnSets.v HahnList.v 
 HahnRelationsBasic.v HahnEquational.v  HahnRewrite.v

diff --git a/descr b/descr
@@ -0,0 +1 @@
+Hahn is a Coq library that contains a useful collection of lemmas and tactics about lists and binary relations.
diff --git a/opam b/opam
@@ -0,0 +1,15 @@
+opam-version: "1.2"
+name: "coq-hahn"
+version: "1.1"
+maintainer: "Anton Podkopaev <[email protected]>"
+authors: "Viktor Vafeiadis <[email protected]>"
+homepage: "https://github.com/vafeiadis/hahn"
+bug-reports: "https://github.com/vafeiadis/hahn/issues"
+license: "MIT"
+dev-repo: "https://github.com/vafeiadis/hahn.git"
+build: [make "-j%{jobs}%"]
+install: [make "-f" "Makefile.coq" "install"]
+remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/hahn"]
+depends: [
+  "coq" { (>= "8.8.1" & < "8.9~") | (= "dev") }
+]
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		Hahn is a Coq library that contains a useful collection of lemmas and tactics about lists and binary relations.