| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | change the flag "internal" in declare/ind_tables from bool to |  vsiles | 2010-06-29 |
| * | New pass on inductive schemes |  herbelin | 2010-05-29 |
| * | Remove the svn-specific $Id$ annotations |  letouzey | 2010-04-29 |
| * | Added a new exception for already declared Schemes, | vsiles | 2010-04-27 |
| * | Fixes in rewrite and a Elimination/Case to Scheme: |  msozeau | 2010-03-06 |
| * | Minor fixes. | msozeau | 2010-03-05 |
| * | Made the side-conditions of lemmas always come last when chaining "apply in" | herbelin | 2009-12-13 |
| * | Quick fix for restoring a left-to-right rewriting lemma compatible | herbelin | 2009-11-09 |
| * | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin | 2009-11-08 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |