incorrect reuse of name in generated case

[south163]

When you use names like n1 and n2 in a context relation definition case analysis on a hypotheses with an existing nominal constant dependency can end up missing a necessary renaming and confuse two separate names. When names such as x and y are used instead the bug does not arise.

The following is a small example which demonstrates the issue.

Kind lfobj type.
Kind lftype type.

Type tm lftype.
Type ty lftype.
Type of lfobj -> lfobj -> lftype.
Type hastype lftype -> lfobj -> o.

Define ctx : olist -> prop by
  ctx nil ;
  nabla n1 n2, ctx (hastype (of n1 T) n2 :: hastype tm n1 :: G) := ctx G.

Theorem t :
  forall G, nabla (x:lfobj), ctx (G x) -> ctx (G x).
induction on 1. intros. case H1 (keep).
  %%% G n1 = nil
  search.
  %%% G n1 = hastype (of n2 (T n1)) n3 :: hastype tm n2 :: G1 n1
  search.
  %%% G n1 = hastype (of n1 T) n1 :: hastype tm n1 :: G1
    % This case uses the name n1 for both items in context which is wrong.
  skip.
  %%% G n1 = hastype (of n1 T) n2 :: hastype tm n1 :: G1
  search.

[chaudhuri]

That ctx definition should not have been allowed because in terms n1, n2 etc. are always parsed as constants, not bound variables.

Thanks for the report.