Hugo Herbelin (Jul 31 2023 at 15:04): Hugo Herbelin (Jul 31 2023 at 15:04):In his talk on teaching Coq to undergraduate students at the Coq workshop, @Pierre Rousselin mentioned the crypticity of intros' error message, that is, currently:
Goal True -> True.
intros H1 H2.
^^^^^^^^^^^^
Error: No product even after head-reduction.
or
Goal True.
intro.
^^^^^
Error: No product even after head-reduction.
or
Goal True.
intros H.
^^^^^^^^
Error: No product even after head-reduction.
or
Goal True.
intros (H1,H2).
^^^^^^^^^^^^^^
Error: No product even after head-reduction.
Pierre proposed "No more variables or hypotheses to introduce". We could actually have two variants, one with "more" and one without (as a matter of comparison, ssr's movesays "No assumption in True"). We should also probably highlight the introduction pattern that cannot be introduced when there is one. However, what would be the best way to attach a location to the error message. At some time, there was the idea that the tactics.mlfile should not mention locs. I guess the alternative is to carefully catch the error at places where it makes sense to attach a location. Any opinion?
Gaëtan Gilbert (Jul 31 2023 at 15:20):At some time, there was the idea that the
tactics.mlfile should not mention locs.
Please explain more
I guess the alternative is to carefully catch the error at places where it makes sense to attach a location.
I think this may be already the case
Hugo Herbelin (Jul 31 2023 at 16:15):Please explain more
PMP was reluctant at some time when I wanted to push the location of idents towards the place errors are raised.
I think this may be already the case
In the case of intros, the error is attached (only) to the tactic call.
Last updated: Dec 05 2023 at 12:01 UTC