| Commit message (Expand) | Author | Age |
|---|
| * | Fix 0 obligations bug |  msozeau | 2006-10-10 |
| * | Add dependent list combinators test. | msozeau | 2006-09-28 |
| * | Report de l'heuristique d'unification premier ordre flexible/rigide |  herbelin | 2006-09-15 |
| * | Fix wrong order for building library, add informative messages. | msozeau | 2006-09-04 |
| * | New handling of obligations. | msozeau | 2006-09-01 |
| * | Forgot to add this one. | 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 |
| * | Mutually structurally recursive defs and rec using measures added. | msozeau | 2006-06-22 |
| * | Wellfounded recursion using subtac working again. | msozeau | 2006-06-20 |
| * | Progress in new wf def typing. | msozeau | 2006-06-20 |
| * | Rewrite of the recursive defs handling in progress. | msozeau | 2006-06-20 |
| * | Correction trou de subject-reduction de create_arg dans genarg.mli | herbelin | 2006-06-07 |
| * | Fix some nasty bug with the evars-to-dependent sum encoding. | msozeau | 2006-06-01 |
| * | The "clean integration of subtac" patch. | msozeau | 2006-05-29 |
| * | - 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-27 |
| * | Added code to support "Program Lemma/Example... etc" | msozeau | 2006-04-16 |
| * | Si un fixpoint a plusieurs arguments, mais un seul de type inductif, |  letouzey | 2006-04-14 |
| * | Test files for subtac. | msozeau | 2006-04-14 |
| * | 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-10 |
| * | - 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 |
| * | Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}. | msozeau | 2006-03-13 |
| * | New files for subtac |  coq | 2006-03-05 |
| * | Work on recursive definitions | coq | 2006-02-22 |
| * | Add vernacular file for subtac | coq | 2006-02-22 |
| * | 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 |
| * | 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-02-20 |
| * | Réorganisation de la structure interne des types de déclarations (decl_kinds) | herbelin | 2006-01-28 |
| * | Restructuration et simplification des fonctions d'affichage, de détypage | herbelin | 2006-01-11 |
| * | 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-26 |
| * | Changement des named_context |  gregoire | 2005-12-02 |
| * | Subtac: traitement correct des existentielles et de la récursion. | coq | 2005-07-15 |
| * | General recursive definitions on well founded orders support | coq | 2005-07-13 |
| * | Add a guard for V7 mode, CVS compiles cleanly again :) | coq | 2005-05-26 |
| * | Added subtac contrib. | coq | 2005-05-25 |
msozeau
herbelin
letouzey
coq
gregoire