The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Hi all,
 is there some particular reason why "rewrite <- H." does "apply eq_ind_r  
..." and not "case H"?
I only see advantages using "case" instead of "rewrite <-":

* proof terms are more readable in general
* it seems it lightens type checking/skips computing a generalization of  
the goal
* it suppress a function call

For rewriting in hypotheses, it is lightly more complex, but realizable.

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay