aboutsummaryrefslogtreecommitdiffhomepage
path: root/.merlin
diff options
context:
space:
mode:
authorGravatar Pierre <pierre.boutillier@ens-lyon.org>2014-01-11 09:22:47 +0100
committerGravatar Pierre <pierre.boutillier@ens-lyon.org>2014-01-11 09:24:33 +0100
commit862214db79059e263d296920079c8d7d88c2049a (patch)
treeb57dfb5f7a812e15ba8c2a7182cdbb6705890287 /.merlin
parenteb8cb1ed86a9c31daba644e1104739795814e4a7 (diff)
'Pretty' printer for wf_paths
Diffstat (limited to '.merlin')
-rw-r--r--.merlin2
1 files changed, 2 insertions, 0 deletions
diff --git a/.merlin b/.merlin
index 929f98e2c..ce5bff525 100644
--- a/.merlin
+++ b/.merlin
@@ -18,6 +18,8 @@ S proofs
B proofs
S tactics
B tactics
+S printing
+B printing
S parsing
B parsing
S toplevel