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. --- interp/stdarg.ml | 2 ++ interp/stdarg.mli | 5 +++++ 2 files changed, 7 insertions(+) (limited to 'interp') diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 5920b0d508..64f8b3913e 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -59,6 +59,8 @@ let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" let wit_constr_with_bindings = make0 "constr_with_bindings" +let wit_open_constr_with_bindings = make0 "open_constr_with_bindings" + let wit_bindings = make0 "bindings" let wit_red_expr = make0 "redexpr" diff --git a/interp/stdarg.mli b/interp/stdarg.mli index ac40a23281..893ec54d45 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -59,6 +59,11 @@ val wit_constr_with_bindings : glob_constr_and_expr with_bindings, constr with_bindings delayed_open) genarg_type +val wit_open_constr_with_bindings : + (constr_expr with_bindings, + glob_constr_and_expr with_bindings, + constr with_bindings delayed_open) genarg_type + val wit_bindings : (constr_expr bindings, glob_constr_and_expr bindings, -- cgit v1.2.3