Mercurial > cpdt > repo

comparison src/StackMachine.v @ 316:2aaff91f5258

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through InductiveTypes, through end of reflexive types
author Adam Chlipala <adam@chlipala.net>
date Sun, 11 Sep 2011 17:22:36 -0400
parents d5787b70cf48
children cbeccef45f4e
comparison
equal deleted inserted replaced
315:72bffb046797 316:2aaff91f5258
843 induction p; crush. 843 induction p; crush.
844 Qed. 844 Qed.
845 845
846 (** This one goes through completely automatically. 846 (** This one goes through completely automatically.
847 847
848 Some code behind the scenes registers [app_assoc_reverse] for use by [crush]. We must register [tconcat_correct] similarly to get the same effect:%\index{Verncular commands!Hint Rewrite}% *) 848 Some code behind the scenes registers [app_assoc_reverse] for use by [crush]. We must register [tconcat_correct] similarly to get the same effect:%\index{Vernacular commands!Hint Rewrite}% *)
849 849
850 (* begin hide *) 850 (* begin hide *)
851 Hint Rewrite tconcat_correct : cpdt. 851 Hint Rewrite tconcat_correct : cpdt.
852 (* end hide *) 852 (* end hide *)
853 (** %\noindent%[Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [tconcat_correct : cpdt.] *) 853 (** %\noindent%[Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [tconcat_correct : cpdt.] *)