| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | New handling of obligations. |  msozeau | 2006-09-01 |
| * | Subtac fixes, new way of handling obligations in progress. | msozeau | 2006-09-01 |
| * | Rewrite of the recursive defs handling in progress. | msozeau | 2006-06-20 |
| * | Fix some nasty bug with the evars-to-dependent sum encoding. | msozeau | 2006-06-01 |
| * | Added code to support "Program Lemma/Example... etc" | msozeau | 2006-04-16 |
| * | - Documentation of the Program tactics. | msozeau | 2006-04-07 |
| * | Subtac fixes, single fixpoint definitions are working again. Added a toggle o... | msozeau | 2006-03-22 |
| * | Made pretyping a functor over a coercion implementation. Pretyping.Default us... | msozeau | 2006-03-22 |
| * | New files for subtac |  coq | 2006-03-05 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |