This Coq-club thread discusses the precise definition of the simpl tactic. The thread is more up-to-date than the corresponding section in the Coq Reference Manual, found here.
This page is down!
simpl (tactic) (last edited 18-07-2010 13:51:42 by oumix)