diff --git a/dune-project b/dune-project
index 882bfcb77..8f51cba77 100644
--- a/dune-project
+++ b/dune-project
@@ -14,41 +14,18 @@
  (name lambdapi)
  (synopsis "Proof assistant for the λΠ-calculus modulo rewriting")
  (description
-"This package provides:
-- A lambdapi command for checking .lp or .dk files,
-translating .dk files to .lp files and vice versa,
-or launching an LSP server for editing .lp files.
-- A library of logic definitions and basic definitions and proofs
-on natural numbers and polymorphic lists.
-- A rich Emacs mode based on LSP (available on MELPA too).
-- A basic mode for Vim.
-- OCaml libraries.
-A VSCode extension is available on the VSCode Marketplace.
 
-Find Lambdapi user manual on https://lambdapi.readthedocs.io/.
+"Lambdapi is an interactive proof assistant for the λΠ-calculus modulo
+rewriting. It can call external automated theorem provers via Why3.
+The user manual is on https://lambdapi.readthedocs.io/.
+A standard library and other developments are available on
+https://github.com/Deducteam/opam-lambdapi-repository/. An extension
+for Emacs is available on MELPA. An extension for VSCode is available
+on the VSCode Marketplace. Lambdapi can read Dedukti files. It
+includes checkers for local confluence and subject reduction. It also
+provides commands to export Lambdapi files to other formats or
+systems: Dedukti, Coq, HRS, CPF.")
 
-Lambdapi provides a rich type system with dependent types.
-In Lambdapi, one can define both type and function symbols
-by using rewriting rules (oriented equations). The declaration
-of symbols and rewriting rules is separated so that one can
-easily define inductive-recursive types for instance.
-Rewrite rules can be exported to the TRS and XTC formats
-for checking confluence and termination with external tools.
-A symbol can be declared associative and commutative.
-Lambdapi supports unicode symbols and infix operators.
-
-Lambdapi does not come with a pre-defined logic. It is a
-powerful logical framework in which one can easily define
-its own logic and build and check proofs in this logic.
-There exist .lp files defining first or higher-order logic
-and complex type systems like in Coq or Agda.
-
-Lambdapi provides a basic module and package system,
-interactive modes for proving both unification goals
-and typing goals, and tactics for solving them step by step.
-In particular, a rewrite tactic like in SSReflect, and
-a why3 tactic for calling external automated provers through
-the Why3 platform.")
  (depends
   (ocaml (>= 4.08.0))
   (menhir (>= 20200624))
diff --git a/lambdapi.opam b/lambdapi.opam
index 154ad7a5c..43bbf5a5c 100644
--- a/lambdapi.opam
+++ b/lambdapi.opam
@@ -1,45 +1,17 @@
-# This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
 synopsis: "Proof assistant for the λΠ-calculus modulo rewriting"
 description: """
-This package provides:
-- A lambdapi command for checking .lp or .dk files,
-translating .dk files to .lp files and vice versa,
-or launching an LSP server for editing .lp files.
-- A library of logic definitions and basic definitions and proofs
-on natural numbers and polymorphic lists.
-- A rich Emacs mode based on LSP (available on MELPA too).
-- A basic mode for Vim.
-- OCaml libraries.
-A VSCode extension is also available on the VSCode Marketplace.
-
-Find Lambdapi user manual on https://lambdapi.readthedocs.io/.
-
-Lambdapi provides a rich type system with dependent types.
-In Lambdapi, one can define both type and function symbols
-by using rewriting rules (oriented equations).
-A symbol can be declared associative and commutative.
-Lambdapi supports unicode symbols and infix operators.
-The declaration of symbols and rewriting rules is separated
-so that one can easily define inductive-recursive types.
-
-Lambdapi checks that rules are locally confluent (by checking
-the joinability of critical pairs) and preserve typing.
-Rewrite rules can also be exported to the TRS and XTC formats
-for checking confluence and termination with external tools.
-
-Lambdapi does not come with a pre-defined logic. It is a
-powerful logical framework in which one can easily define
-its own logic and build and check proofs in this logic.
-There exist .lp files defining first or higher-order logic
-and complex type systems like in Coq or Agda.
-
-Lambdapi provides a basic module and package system,
-interactive modes for proving both unification goals
-and typing goals, and tactics for solving them step by step.
-In particular, a rewrite tactic like in SSReflect, and
-a why3 tactic for calling external automated provers through
-the Why3 platform."""
+Lambdapi is an interactive proof assistant for the λΠ-calculus modulo
+rewriting. It can call external automated theorem provers via Why3.
+The user manual is on https://lambdapi.readthedocs.io/.
+A standard library and other developments are available on
+https://github.com/Deducteam/opam-lambdapi-repository/. An extension
+for Emacs is available on MELPA. An extension for VSCode is available
+on the VSCode Marketplace. Lambdapi can read Dedukti files. It
+includes checkers for local confluence and subject reduction. It also
+provides commands to export Lambdapi files to other formats or
+systems: Dedukti, Coq, HRS, CPF.
+"""
 maintainer: ["dedukti-dev@inria.fr"]
 authors: ["Deducteam"]
 license: "CECILL-2.1"
@@ -79,4 +51,5 @@ build: [
     "@doc" {with-doc}
   ]
 ]
-available: arch != "ppc64"
+conflicts: [ "ocaml-option-bytecode-only" ]
+