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.

5 files changed, 19 insertions, 7 deletions

diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 2d1220385a..28ff6df838 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 a3b3fae0b3..bd48614dbc 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
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 15cef676e6..e41236b1c3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2966,10 +2966,6 @@ let specialize (c,lbind) ipat =
   let env = Proofview.Goal.env gl in
   let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
   let sigma, term =
-    if lbind == NoBindings then
-      let sigma = Typeclasses.resolve_typeclasses env sigma in
-      sigma, nf_evar sigma c
-    else
       let clause = make_clenv_binding env sigma (c,Retyping.get_type_of env sigma c) lbind in
       let flags = { (default_unify_flags ()) with resolve_evars = true } in
       let clause = clenv_unify_meta_types ~flags clause in
diff --git a/test-suite/bugs/closed/5153.v b/test-suite/bugs/closed/5153.v
new file mode 100644
index 0000000000..be6407b5fa
--- /dev/null
+++ b/test-suite/bugs/closed/5153.v
@@ -0,0 +1,8 @@
+(* An example where it does not hurt having more type-classes resolution *)
+Class some_type := { Ty : Type }.
+Instance: some_type := { Ty := nat }.
+Arguments Ty : clear implicits.
+Goal forall (H : forall t : some_type, @Ty t -> False) (H' : False -> 1 = 2), 1 = 2.
+Proof.
+intros H H'.
+specialize (H' (@H _ O)). (* was failing *)
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index fba05cd902..4b41a509e5 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -72,3 +72,11 @@ intros.
 specialize (H 1) as ->.
 reflexivity.
 Qed.
+
+(* A test from corn *)
+
+Goal (forall x y, x=0 -> y=0 -> True) -> True.
+intros.
+specialize (fun z => H 0 z eq_refl).
+exact (H 0 eq_refl).
+Qed.