| Age | Commit message (Expand) | Author |
|---|
| 2006-06-01 | Fix some nasty bug with the evars-to-dependent sum encoding. | msozeau |
| 2006-05-29 | The "clean integration of subtac" patch. | msozeau |
| 2006-04-27 | - Distinction explicite des parties paramètres et arguments dans le type | herbelin |
| 2006-04-27 | Standardisation nom option_app en option_map | herbelin |
| 2006-04-16 | Added code to support "Program Lemma/Example... etc" | msozeau |
| 2006-04-14 | Si un fixpoint a plusieurs arguments, mais un seul de type inductif, | letouzey |
| 2006-04-14 | Test files for subtac. | msozeau |
| 2006-04-10 | Fixes for new unification, not used in default version as it really changes u... | msozeau |
| 2006-04-10 | Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous... | msozeau |
| 2006-04-07 | - Documentation of the Program tactics. | msozeau |
| 2006-03-22 | 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-13 | Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}. | msozeau |
| 2006-03-05 | New files for subtac | coq |
| 2006-02-22 | Work on recursive definitions | coq |
| 2006-02-22 | Add vernacular file for subtac | coq |
| 2006-02-21 | 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-20 | Fix minor bug | coq |
| 2006-02-20 | Forgot a file | coq |
| 2006-02-20 | Monday work, working with coercions and implicit args | coq |
| 2006-02-20 | Forgot another file... | coq |
| 2006-02-20 | Forgot one file | coq |
| 2006-02-20 | Rewrite of the subtac tactic, needs some work on implicit arguments. | coq |
| 2006-01-28 | Réorganisation de la structure interne des types de déclarations (decl_kinds) | herbelin |
| 2006-01-11 | Restructuration et simplification des fonctions d'affichage, de détypage | herbelin |
| 2005-12-26 | Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*... | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme... | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-07-15 | Subtac: traitement correct des existentielles et de la récursion. | coq |
| 2005-07-13 | General recursive definitions on well founded orders support | coq |
| 2005-05-26 | Add a guard for V7 mode, CVS compiles cleanly again :) | coq |
| 2005-05-25 | Added subtac contrib. | coq |
