| Age | Commit message (Expand) | Author |
|---|---|---|
| 2007-08-07 | Move Program tactics into a proper theories/ directory as they are general pu... | msozeau |
| 2007-07-19 | Documentation of Program and its tactics, fix enormous interaction bug due to... | msozeau |
| 2007-02-28 | The right tactics for definitions using measures. | msozeau |
| 2007-01-29 | Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes. | msozeau |
| 2007-01-08 | Subtac fixes, support for reasoning on wf defs. | msozeau |
| 2006-06-22 | Mutually structurally recursive defs and rec using measures added. | msozeau |
| 2006-04-10 | Fixes for new unification, not used in default version as it really changes u... | msozeau |
| 2006-04-07 | - Documentation of the Program tactics. | msozeau |
| 2006-03-22 | Made pretyping a functor over a coercion implementation. Pretyping.Default us... | msozeau |
| 2006-03-13 | Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}. | msozeau |
| 2006-02-22 | Add vernacular file for subtac | coq |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |