Need specific messages for semantic restrictions in the "destruct" tactic.

[jfehrle]

I noticed some odd handling of semantic restrictions in "destruct" that we may want to clean up.

• The action routine for induction_clause_list applies a semantic restriction, for which it calls err, raising Stream.Failure, which is misleadingly reported as a syntax error. For example, destruct x at 1 using H at 1. gives Syntax error: [induction_clause_list] expected after 'destruct' (in [simple_tactic]). The semantic restriction should be reported with a specific message, e.g. "'at' clause not permitted here; the destruction argument already has an 'at' clause"
• The opt_clause on the end of induction_clause_list is not permitted (Ex: destruct x, y using H at 1) when there is more than one destruction_arg. This should probably get a separate specific message. I expect this opt_clause was added as a syntactic convenience for users, but it seems somewhat limited in its applicability and requires a bit of extra description in the doc.

I suggest we should give specific messages for these rather than syntax errors.

[jfehrle]

Also, the grammar in the screenshot is clearly ambiguous (though AFAIK the parser does the right thing)!

Attn: @herbelin @Zimmi48

[jfehrle]

Also notice that the screenshot grammar suggests that destruct x at 1 at 2. is valid, which is not.

[Zimmi48]

The semantic restriction should be reported with a specific message, e.g. "'at' clause not permitted here; the destruction argument already has an 'at' clause"

I agree that semantic error messages are generally clearer (and thus preferable) to parsing errors.

The opt_clause should be a goal_occurrences in the documented grammar (and probably even in the code?). And I don't understand why its use is restricted. Maybe this limitation could be lifted?