aboutsummaryrefslogtreecommitdiff
path: root/lib/lib.mllib
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-07-24 11:03:52 +0200
committerEmilio Jesus Gallego Arias2018-07-24 11:03:52 +0200
commit4ab54f3cca76632cb6e258c84abc259e15e9e9f8 (patch)
treec4374a0986acd6d4f6cac1a03e6bfa5ba7c972c9 /lib/lib.mllib
parent580a026070ab74d05f38e1177632be83a8756566 (diff)
parent97069f69ab3a58cc4ccbaa1a835912c6c31dde4d (diff)
Merge PR #6801: Highlight differences between successive proof steps (color, underline, etc.)
Diffstat (limited to 'lib/lib.mllib')
-rw-r--r--lib/lib.mllib1
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 0891859423..41b3622a99 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -6,6 +6,7 @@ Control
Util
Pp
+Pp_diff
Stateid
Loc
Feedback