aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Tej Chajed <tchajed@mit.edu>2017-02-16 10:24:15 -0500
committerGravatar Tej Chajed <tchajed@mit.edu>2017-02-16 13:49:11 -0500
commite6127d1f65a761a27c80b81c0f1bc5fca2b74af8 (patch)
tree9c839d3ef53da61f50a1c044d6120c3f5e363de8 /dev
parentbcb634d070519d6e37d9b7d39f12437a7d38f0c2 (diff)
[cleanup] Change Id.t option to Name.t in TacFun
Diffstat (limited to 'dev')
-rw-r--r--dev/doc/changes.txt3
1 files changed, 3 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index f54f3fcc8..2a083b360 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -40,6 +40,9 @@ important things:
- Some printing functions were moved from Pptactic to Pputils
- A part of Tacexpr has been moved to Tactypes
+The TacFun tactic expression constructor now takes a `Name.t list` for the
+variable list rather than an `Id.t option list`.
+
** Error handling **
- All error functions now take an optional parameter `?loc:Loc.t`. For