diff options
Diffstat (limited to 'plugins/ltac/extratactics.ml4')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index a3b3fae0b..bd48614db 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -190,7 +190,7 @@ let onSomeWithHoles tac = function | Some c -> Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> tac (Some c)) TACTIC EXTEND contradiction - [ "contradiction" open_constr_with_bindings_opt(c) ] -> + [ "contradiction" constr_with_bindings_opt(c) ] -> [ onSomeWithHoles contradiction c ] END |