Improving error message for clear tactic (and indirect uses of it).

- Be more precise when trying to clear an hypothesis which
  occurs implicitly in a global constant.
- Warns if destruct/induction cannot clear an hypothesis occurring
  implicitly in a global.

In the first case, the change in situation

  Section A. Variable a:nat. Definition b:=a=a. Goal b=b. clear a.

is:

- before: "a is used in conclusion"
- after: "a is used implicitly in b in conclusion"

In the second case:

  Section A. Variable a:nat. Definition b:=a=a. Goal b=b. destruct a.

produces a warning: "Cannot remove a, it is used implicitly in b".

0 files changed, 0 insertions, 0 deletions