The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I attempted to write a tactic that would lower the universe level of an 
equality conclusion, so as to avoid these problems - but it has a 
problem of its own:

Variable S1 S2 : Set.

Ltac lowereq :=
lazymatch goal with
(*replace any equality by a min-universe-leveled one*)
|- @eq _ ?X ?Y => assert (X = Y) as H; [|rewrite H; reflexivity]
end.

Goal @eq Type S1 S1.
Fail lowereq. (*Error: Tactic generated a subgoal identical to the 
original goal*)
Admitted.

Goal @eq Type S1 S2.
lowereq. (*works properly*)
lowereq. (*no complaints about identical subgoals here*)
Admitted.

Why does Coq complain about a subgoal being identical to the original in 
the first Goal case?  It doesn't do that elsewhere (as the second Goal 
shows).  What is it trying to prevent?  Isn't that a job for the 
progress tactical?

-- Jonathan