| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | Added Chung-Kil Hur's smart "pattern" tactic (h_resolve). |  herbelin | 2010-06-22 |
| * | Added rudimentary support for using constructors from the explicit | herbelin | 2010-06-12 |
| * | Fix bug 2307 |  pboutill | 2010-05-20 |
| * | Remove the svn-specific $Id$ annotations |  letouzey | 2010-04-29 |
| * | Continuing r12485-12486 and r12549 (cleaning around name generation) | herbelin | 2009-12-02 |
| * | Continuing r12485-12486 (cleaning around name generation) | herbelin | 2009-12-01 |
| * | Added support for definition of fixpoints using tactics. | herbelin | 2009-11-27 |
| * | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin | 2009-11-09 |
| * | This big commit addresses two problems: |  soubiran | 2009-10-21 |
| * | Delete trailing whitespaces in all *.{v,ml*} files |  glondu | 2009-09-17 |
| * | Ensures that let-in's in arities of inductive types work well. Maybe not | herbelin | 2009-08-11 |
| * | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin | 2009-08-06 |
| * | - Fixing bug #2084 (unification not checking sort constraints), hoping | herbelin | 2009-04-08 |
| * | - Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing | herbelin | 2009-04-08 |
| * | Compromise wrt introduction-names compatibility issue after addition | herbelin | 2009-03-22 |
| * | DISCLAIMER |  puech | 2009-01-17 |
| * | Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod -> | herbelin | 2008-12-31 |
| * | fixing problem with CompCert: reordering resulting from tac change was not cl... |  barras | 2008-11-27 |
| * | Fix in the unification algorithm using evars: unify types of evar |  msozeau | 2008-11-05 |
| * | Fixes and refinements regarding occurrence selection: | herbelin | 2008-10-26 |
| * | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin | 2008-10-18 |
| * | * Fixed constr_cmp again to handle universes subtyping correctly | puech | 2008-10-09 |
| * | Fixing constr_cmp, propagating subtyping only right of a product | puech | 2008-10-02 |
| * | Fix a bug, in fold_constr_with_binders, the types of fixpoints were | msozeau | 2008-09-13 |
| * | Report des commits 11297 et 11299 (nom Unnamed_theorem local caché par | herbelin | 2008-08-04 |
| * | Backport r11289. | msozeau | 2008-07-29 |
| * | Uniformisation du format des messages d'erreur (commencent par une | herbelin | 2008-07-17 |
| * | - Implantation de la suggestion 1873 sur discriminate. Au final, | herbelin | 2008-06-21 |
| * | Correction bug 1878 (utilisation de extend_evar déplacée là où une | herbelin | 2008-06-14 |
| * | Correction de deux bugs liés au commit 11094 sur les clauses "at" et "in". | herbelin | 2008-06-11 |
| * | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin | 2008-06-10 |
| * | introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha... | barras | 2008-05-28 |
| * | Changement de stratégie vis à vis du commit 10859 sur la gestion des | herbelin | 2008-05-12 |
| * | - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait des | herbelin | 2008-05-10 |
| * | Réutilisation de l'infrastructure pour le polymorphisme d'univers des | herbelin | 2008-04-30 |
| * | Petites corrections vis à vis des commits 10860, 10859, 10850 | herbelin | 2008-04-28 |
| * | Correction du bug des types singletons pas sous-type de Set | herbelin | 2008-04-27 |
| * | * Factorizing code : context_chop was used in several files (even as chop_con... |  vsiles | 2008-03-17 |
| * | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin | 2007-10-03 |
| * | Suppression des type_app et body_of_type qui alourdissent inutilement le code | herbelin | 2007-08-27 |
| * | - Ajout de la possibilité d'utiliser la notation Record pour les | herbelin | 2007-06-30 |
| * | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin | 2007-05-22 |
| * | Confusion sur le paramètre à donner à concrete_name lors du commit 9450 | herbelin | 2006-12-14 |
| * | Alignement de la politique de renommage de rename_bound_var (utilisé pour | herbelin | 2006-12-13 |
| * | Correction bug #1041 (double cause : non évitement des noms existants en | herbelin | 2006-12-12 |
| * | Évitement des noms de constructeurs dans les motifs de filtrage de "match" | herbelin | 2006-12-09 |
| * | Compatibilité du polymorphisme de constantes avec les sections. | herbelin | 2006-10-29 |
| * | Déplacement de on_judgment_type de Typeops vers Termops | herbelin | 2006-10-06 |
| * | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin | 2006-05-23 |
| * | Standardisation nom option_app en option_map | herbelin | 2006-04-27 |
herbelin
pboutill
letouzey
soubiran
glondu
puech
barras
msozeau
vsiles