| Commit message (Expand) | Author | Age |
|---|
| * | Postpone the search for the recursive argument index from the user given |  msozeau | 2008-05-06 |
| * | - Fix bug in eterm which was not taking filtered contexts in evars into | msozeau | 2008-04-25 |
| * | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau | 2007-12-31 |
| * | Plus de combinateurs sont passés de Util à Option. Le module Options |  aspiwack | 2007-12-06 |
| * | Fix some bugs, add possibility of automatically solving a proof statement's o... | msozeau | 2007-10-24 |
| * | Documentation of Program and its tactics, fix enormous interaction bug due to... | msozeau | 2007-07-19 |
| * | An optimization to simplify generated obligations removing unnecessary let-in's. | msozeau | 2007-07-12 |
| * | Cleanup, use Util list functions when possible | msozeau | 2007-07-12 |
| * | Add a parameter to QuestionMark evar kind to say it can be turned into an obl... | msozeau | 2007-03-19 |
| * | Opacity parameterization for obligations working. | msozeau | 2007-02-24 |
| * | Debug wellfounded defs, work on cleaning obls envs | msozeau | 2007-02-23 |
| * | Various subtac fixes. | msozeau | 2007-01-15 |
| * | Work on mutual defs, various bug fixes. | msozeau | 2006-11-10 |
| * | Debug obligation handling code | msozeau | 2006-10-31 |
| * | Work on obligation separation. | msozeau | 2006-10-31 |
| * | New handling of obligations. | msozeau | 2006-09-01 |
| * | Subtac fixes, new way of handling obligations in progress. | msozeau | 2006-09-01 |
| * | Fix wrong order of existentials in eterm. | msozeau | 2006-06-23 |
| * | Fix some nasty bug with the evars-to-dependent sum encoding. | msozeau | 2006-06-01 |
| * | Standardisation nom option_app en option_map |  herbelin | 2006-04-27 |
| * | - 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 |
| * | Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}. | msozeau | 2006-03-13 |
| * | Work with binder lists, problem of tycons |  coq | 2006-02-21 |
| * | Latest fixes, should work fine now for non recursive definitions, although st... | coq | 2006-02-21 |
| * | Rewrite of the subtac tactic, needs some work on implicit arguments. | coq | 2006-02-20 |
| * | Changement des named_context |  gregoire | 2005-12-02 |
| * | Subtac: traitement correct des existentielles et de la récursion. | coq | 2005-07-15 |
msozeau
aspiwack
herbelin
coq
gregoire