diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-23 21:26:20 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-22 12:06:59 +0200 |
| commit | 9eb2f7480de8ded94a1b96eb4f6cc16d19a8c14d (patch) | |
| tree | 70115d49a0ca45c6fa06a5978878ccb7ae302987 /interp/stdarg.ml | |
| parent | 11851daee3a14f784cc2a30536a8f69be62c4f62 (diff) | |
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.
Diffstat (limited to 'interp/stdarg.ml')
| -rw-r--r-- | interp/stdarg.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 5920b0d50..64f8b3913 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" |