Hi, I'm wondering what the difference is for the inference of implicit parameters for the `destruct`

, `case:`

and `case`

tactics.

For example:

```
From mathcomp Require Import eqtype ssrbool ssreflect.
Parameter T : eqType.
Parameters x y : T.
Goal x = y \/ x != y.
Proof.
(* This fails with "Cannot infer the implicit parameter T of eqVneq whose type is "eqType" " *)
destruct (eqVneq).
Abort.
Goal x = y \/ x != y.
Proof.
(* This succeeds *)
case (eqVneq).
Abort.
```

Where can I find information regarding this process for related questions?

I am sure you have already looked at the Coq manual (destruct tactics and the ssreflect documentation).

Maybe there are relevant comments in the source code of the ssreflect plugin (file coq/plugins/ssr/ssrelim.ml ?).

In any case, `eqVneq`

has been developped and tested to be used with ssreflect `case:`

, using it with ltac `case`

or `destruct`

might or might not work, that's pure luck.

Last updated: Jul 25 2024 at 16:02 UTC