From df7a88408c357141cb9df50af41f7b7776be0e34 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Thu, 29 Dec 2016 22:20:02 -0600
Subject: [PATCH] added local OPAM files

---
 descr |  5 +++++
 opam  | 17 +++++++++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 descr
 create mode 100644 opam

diff --git a/descr b/descr
new file mode 100644
index 0000000..8468a2d
--- /dev/null
+++ b/descr
@@ -0,0 +1,5 @@
+InfSeqExt
+
+InfSeqExt is collection of Coq libraries for reasoning inductively and coinductively on infinite sequences, using modal operators similar to those in linear temporal logic (LTL).
+
+It is intended as a more comprehensive alternative to Streams in the Coq standard library. In particular, InfSeqExt provides machinery commonly used when reasoning about temporal properties of system execution traces, and follows the modal operator name conventions used in the Spin model checker.
diff --git a/opam b/opam
new file mode 100644
index 0000000..d3d6b54
--- /dev/null
+++ b/opam
@@ -0,0 +1,17 @@
+opam-version: "1.2"
+name: "InfSeqExt"
+version: "dev"
+maintainer: "palmskog@gmail.com"
+
+homepage: "https://github.com/DistributedComponents/InfSeqExt"
+dev-repo: "https://github.com/DistributedComponents/InfSeqExt.git"
+bug-reports: "https://github.com/DistributedComponents/InfSeqExt/issues"
+license: "Proprietary"
+
+build: [ [ "./configure" ] [ make "-j%{jobs}%" ] ]
+install: [ make "install" ]
+remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/InfSeqExt" ]
+depends: [ "coq" {((>= "8.5" & < "8.6~") | (>= "8.6" & < "8.7~"))} ]
+
+tags: [ "keyword:temporal logic" "keyword:infinite transition systems" "keyword:coinduction" "category:Mathematics/Logic/Modal logic" ]
+authors: [ "Yuxin Deng <>" "Jean-Francois Monin <>" "Karl Palmskog <>" ]