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: Oct 13 2024 at 01:02 UTC