aboutsummaryrefslogtreecommitdiffhomepage
path: root/.merlin
diff options
context:
space:
mode:
authorGravatar Matej Kosik <matej.kosik@inria.fr>2016-10-28 11:48:46 +0200
committerGravatar Matej Kosik <matej.kosik@inria.fr>2016-11-03 09:26:43 +0100
commit9c52d25ac0badc5ec6eb0eb897219e607c362e83 (patch)
treeda5fdc825cf46b32b6fe8519ad46b2b710f4b0bd /.merlin
parent19a2dd5cfbd72defe932656a65ab9da9f4ac9d1e (diff)
updating ".merlin" file
Diffstat (limited to '.merlin')
-rw-r--r--.merlin2
1 files changed, 2 insertions, 0 deletions
diff --git a/.merlin b/.merlin
index 7ae642233..7279a098e 100644
--- a/.merlin
+++ b/.merlin
@@ -1,5 +1,7 @@
FLG -rectypes -thread
+S ltac
+B ltac
S config
B config
S lib