From 9f3c5ac9243855825f62b0b06a87623623f56961 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Sat, 4 Apr 2020 17:30:31 +0200
Subject: [PATCH] no dirs local, requirements

---
 .dir-locals.el |  2 --
 README.md      | 48 +++---------------------------------------------
 2 files changed, 3 insertions(+), 47 deletions(-)

diff --git a/.dir-locals.el b/.dir-locals.el
index 2034bc9..3b43ed0 100644
--- a/.dir-locals.el
+++ b/.dir-locals.el
@@ -1,5 +1,3 @@
 ;;; Directory Local Variables
 ;;; For more information see (info "(emacs) Directory Variables")
 
-((lambdapi-mode
-  (eval define-abbrev local-abbrev-table "subtype" "⊑" nil :system t)))
diff --git a/README.md b/README.md
index a9937b7..ac05d9b 100644
--- a/README.md
+++ b/README.md
@@ -13,8 +13,8 @@ library, also known as _Prelude_. The prelude is available
 
 
 ## Requirements
-- [`lambdapi`](https://github.com/gabrielhdt/lambdapi.git) on the `heavy-let`
-  branch
+[`lambdapi`](https://github.com/Deducteam/lambdapi.git) later than 
+fda8752584af52cdc8158a7a80bbe7fce5720616
 
 ## Structure
 - `adlib` contains additional libraries not in the prelude
@@ -23,46 +23,4 @@ library, also known as _Prelude_. The prelude is available
 - `prelude` contains parts of the PVS prelude
 - `sandbox` contains miscellaneous experiments
 - `tools` contains some additional scripts and utilities
-- `alternativs` contains files in other encodings
-
-## Emacs abbreviations
-The `.dir-locals.el` activates the `abbrev-mode` when opening a Dedukti file,
-and calls a `set-local-abbrevs` function.
-
-The
-[`abbrev-mode`](https://www.gnu.org/software/emacs/manual/html_node/emacs/Abbrevs.html)
-is used to expand some defined character sequences into longer words.
-The typical example is to expand `btw` to `by the way`.
-The function `set-local-abbrevs` is not built in emacs and 
-allows to define abbreviation locally to a loaded file, 
-otherwise, abbreviations would be saved and activated for all
-Dedukti buffers. The function takes as argument a list of abbreviations.
-
-The code of `set-local-abbrevs` comes from
-<https://stackoverflow.com/questions/21836527/abbrev-local-to-document-in-emacs>
-``` emacs-lisp
-(defun set-local-abbrevs (abbrevs)
-    "Add ABBREVS to `local-abbrev-table' and make it buffer local.
-     ABBREVS should be a list of abbrevs as passed to `define-abbrev-table'.
-     The `local-abbrev-table' will be replaced by a copy with the new 
-     abbrevs added, so that it is not the same as the abbrev table used
-     in other buffers with the same `major-mode'."
-    (let* ((bufname (buffer-name))
-           (prefix (substring (md5 bufname) 0 (length bufname)))
-           (tblsym (intern (concat prefix "-abbrev-table"))))
-      (set tblsym (copy-abbrev-table local-abbrev-table))
-      (dolist (abbrev abbrevs)
-          (define-abbrev (eval tblsym)
-            (car abbrev)
-            (cadr abbrev)
-            (caddr abbrev)))
-    (setq-local local-abbrev-table (eval tblsym))))
-```
-
-And we define the following abbreviations,
-
-| Key sequence | Expansion |
-|:-------------|----------:|
-| subtype      |         ⊑ |
-| upcast       |         ↑ |
-| downcast     |         ↓ |
+- `alternatives` contains files in other encodings
-- 
GitLab