diff --git a/CHANGELOG.md b/CHANGELOG.md
deleted file mode 100644
index 8c6e5267..00000000
--- a/CHANGELOG.md
+++ /dev/null
@@ -1,87 +0,0 @@
-# CHANGES
-
-## 0.6.1
-
-- add simple functor for DOT backend
-- various bugfixes
-
-## 0.6
-
-### Feature
-
-- An already instantiated sat solver in the Sat module
-- A `full_slice` function for running possibly expensive satisfiability
-  tests (in SMT) when a propositional model has been found
-- Forgetful propagations: propagations whose reason (i.e clause) is not watched
-
-## 0.5.1
-
-### Bug
-
-- Removed some needless allocations
-
-### Breaking
-
-- Better interface for mcsat propagations
-
-### Feature
-
-- Allow level 0 semantic propagations
-
-## 0.5
-
-### Bug
-
-- Grow heap when adding local hyps
-- Avoid forgetting some one atom clauses
-- Fixed a bug for propagations at level 0
-- Late propagations need to be re-propagated
-- Fixed conflict at level 0
-- Avoid forgetting some theory conflict clauses
-
-### Breaking
-
-- Changed `if_sat` interface
-
-## 0.4.1
-
-### Bug
-
-- fix bug in `add_clause`
-
-## 0.4
-
-- performance improvements
-- many bugfixes
-- more tests
-
-### Breaking
-
-- remove push/pop (source of many bugs)
-- replaced by solve : assumptions:lit list -> unit -> result
-
-### Features
-
-- Accept late conflict clauses
-- cleaner API, moving some types outside the client-required interface
-
-## 0.3
-
-### Features
-
-- Proofs for atoms at level 0
-- Compatibility with ocaml >= 4.00
-- Released some restrictions on dummy sat theories
-
-## 0.2
-
-### Breaking
-
-- Log argument has been removed from functors
-- All the functors now take a dummy last argument to ensure the solver modules are unique
-
-### Features
-
-- push/pop operations
-- access to decision level when evaluating literals
-
diff --git a/VERSION b/VERSION
deleted file mode 100644
index 5a2a5806..00000000
--- a/VERSION
+++ /dev/null
@@ -1 +0,0 @@
-0.6