From 9eb2f7480de8ded94a1b96eb4f6cc16d19a8c14d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 23 Oct 2016 21:26:20 +0200 Subject: Clarifying the interpretation path for the "constr_with_binding" argument. This fixes an inconsistency introduced in 554a6c806 (svn r12603) where both interp_constr_with_bindings and interp_open_constr_with_bindings were going through interp_open_constr (no type classes so as to not to commit too early on irreversible choices, accepting unresolved holes). We fix this by having interp_constr_with_bindings going to interp_constr (using type classes and failing on unresolved evars). The external impact is that any TACTIC EXTEND which refers to constr_with_binding has now to decide whether it intends it to use what the name suggest (using type classes and to fail if evars remain unresolved), thus keeping constr_with_binding, or the actual behavior which requires to use open_constr_with_bindings for strict compatibility. --- dev/doc/changes.txt | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'dev/doc/changes.txt') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 8ea1638c9..7db5647c3 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -93,6 +93,12 @@ alternative solution would be to fully qualify Ltac modules, e.g. turning any call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not work for EXTEND macros though. +** Additional changes in tactic extensions ** + +Entry "constr_with_bindings" has been renamed into +"open_constr_with_bindings". New entry "constr_with_bindings" now +uses type classes and rejects terms with unresolved holes. + ** Error handling ** - All error functions now take an optional parameter `?loc:Loc.t`. For -- cgit v1.2.3