From 9f463c144c54a013a0ee214383391f9fc48259d9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 24 Oct 2016 11:29:52 +0200 Subject: 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. --- plugins/ltac/coretactics.ml4 | 4 ++-- plugins/ltac/extratactics.ml4 | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins') 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 -- cgit v1.2.3