prepare for 1.5.1

CHANGELOG.md

@@ -1,5 +1,38 @@
 # Changelog
 
+## 1.5.1
+
+- compatibility with ocaml 4.08
+- move to sneeuwballen organization
+- migrate to dune
+- changes in HO
+- use msat.0.8
+- migrate to `iter` instead of `sequence`
+- make build a bit more robust wrt warn-error
+- add travis CI
+
+- perf improvements
+- perf: use profile=release
+- make floor (and co) a function from real to real
+- two bugfixes for polymorphic function types
+- fix(demo): update resolution demo so it builds again
+- fix(superposition): do not try to rewrite type arguments
+- chore: update opam files to 2.0
+- move to alcotest for tests
+- improve ho selection restrictions
+- perf: optimize `debugf` function (closes #21)
+- support more cases in THF parser
+- less selection restrictions for lfhol-calculi
+- cli option for fool
+- bugfix: KBO variable balance for applied variables
+- In TPTP, interpret untyped variables as $i, not as a fresh type variable
+- Don't rewrite heads in subsumption module
+- complete variables one-by-one in complete_eq_args (ArgCong)
+- dont rewrite heads in the presence of type variables or nonmonotonicity
+- loosen assertion in whnf_deref_rec
+- Use type arguments in orderings
+- missing supatvars flag should switch off hidden supatvars
+
 ## 1.5
 
 - be compatible with sequence >= 1.0

libzipperposition.opam

@@ -2,7 +2,7 @@ opam-version: "2.0"
 maintainer: "[email protected]"
 author: "Simon Cruanes"
 homepage: "https://github.com/sneeuwballen/zipperposition"
-version: "1.5"
+version: "1.5.1"
 synopsis: "Library for Zipperposition"
 build: [
   ["dune" "build" "-p" name]
@@ -12,7 +12,7 @@ depends: [
   "base-bytes"
   "base-unix"
   "zarith"
-  "logtk" { >= "1.5" }
+  "logtk" { = version }
   "containers" { >= "1.0" }
   "iter" { >= "1.2" }
   "dune" { build }

logtk.opam

@@ -2,7 +2,7 @@ opam-version: "2.0"
 maintainer: "[email protected]"
 author: "Simon Cruanes"
 homepage: "https://github.com/sneeuwballen/zipperposition"
-version: "1.5"
+version: "1.5.1"
 synopsis: "Core types and algorithms for logic"
 build: [
   ["dune" "build" "-p" name]

zipperposition-tools.opam

@@ -2,7 +2,7 @@ opam-version: "2.0"
 maintainer: "[email protected]"
 author: "Simon Cruanes"
 homepage: "https://github.com/sneeuwballen/zipperposition"
-version: "1.5"
+version: "1.5.1"
 synopsis: "Support tools for Zipperposition"
 build: [
   ["dune" "build" "-p" name]
@@ -14,8 +14,8 @@ depends: [
   "iter" { >= "1.2" }
   "msat" { >= "0.8" < "0.9" }
   "zarith"
-  "logtk" { >= "1.5" }
-  "libzipperposition" { >= "1.5" }
+  "logtk" { = version }
+  "libzipperposition" { = version }
   "ocaml" {>= "4.03"}
 ]
 bug-reports: "https://github.com/sneeuwballen/zipperposition/issues"

zipperposition.opam

@@ -2,7 +2,7 @@ opam-version: "2.0"
 maintainer: "[email protected]"
 author: "Simon Cruanes"
 homepage: "https://github.com/sneeuwballen/zipperposition"
-version: "1.5"
+version: "1.5.1"
 synopsis: "A fully automatic theorem prover for typed first-order and beyond"
 build: [
   ["dune" "build" "-p" name]
@@ -11,8 +11,8 @@ build: [
 depends: [
   "base-unix"
   "zarith"
-  "logtk" { >= "1.5" }
-  "libzipperposition" { >= "1.5" }
+  "logtk" { = version }
+  "libzipperposition" { = version }
   "containers" { >= "1.0" }
   "iter" { >= "1.2" }
   "dune" { build }