diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-24 11:29:52 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-22 12:06:59 +0200 |
| commit | 9f463c144c54a013a0ee214383391f9fc48259d9 (patch) | |
| tree | e897efafe48d53239e07309915d888184067ef4e /plugins | |
| parent | 9eb2f7480de8ded94a1b96eb4f6cc16d19a8c14d (diff) | |
Using type classes in the interpretation of "specialize" and "contradiction".
We do that by using constr_with_bindings rather than
open_constr_with_bindings (+ extra call to typeclasses in
"specialize"). If my understanding is right, the only effect would be
to succeed more in cases where it was failing (in
inh_conv_coerce_to_gen). In particular, "specialize" and
"contradiction" already have a WITHHOLES test for rejecting pending
holes.
Incidentally, this answers enhancement #5153.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/coretactics.ml4 | 4 | ||||
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 2d1220385..28ff6df83 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -141,10 +141,10 @@ END (** Specialize *) TACTIC EXTEND specialize - [ "specialize" open_constr_with_bindings(c) ] -> [ + [ "specialize" constr_with_bindings(c) ] -> [ Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None) ] -| [ "specialize" open_constr_with_bindings(c) "as" intropattern(ipat) ] -> [ +| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [ Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat)) ] END 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 |