added local OPAM files

Author: palmskog

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.

opam

@@ -0,0 +1,17 @@
+opam-version: "1.2"
+name: "InfSeqExt"
+version: "dev"
+maintainer: "[email protected]"
+
+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 <>" ]