| Commit message (Expand) | Author | Age |
|---|
| * | More {raw => glob} changes for consistency |  glondu | 2010-12-24 |
| * | Rename rawterm.ml into glob_term.ml | glondu | 2010-12-23 |
| * | Change of nomenclature: rawconstr -> glob_constr | glondu | 2010-12-23 |
| * | Some dead code removal, thanks to Oug analyzer |  letouzey | 2010-09-24 |
| * | Updated all headers for 8.3 and trunk |  herbelin | 2010-07-24 |
| * | Extension of the recursive notations mechanism | herbelin | 2010-07-22 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | Fixing bug #2279 (printing nested let-in was in exponential time) | herbelin | 2010-03-27 |
| * | fixed confusion between number of cstr arguments and number of pattern variab... |  barras | 2010-03-12 |
| * | In "simpl c" and "change c with d", c can be a pattern. | herbelin | 2009-12-24 |
| * | Continuing r12485-12486 (cleaning around name generation) | herbelin | 2009-12-01 |
| * | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin | 2009-11-09 |
| * | Took local definitions into account in the test for deciding whether | herbelin | 2009-11-08 |
| * | This big commit addresses two problems: |  soubiran | 2009-10-21 |
| * | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
| * | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin | 2009-08-06 |
| * | Improved parameterization of Coq: | herbelin | 2009-08-02 |
| * | Rewrite of Program Fixpoint to overcome the previous limitations: |  msozeau | 2009-03-28 |
| * | Move Record desugaring to constrintern and add ability to use notations | msozeau | 2008-11-05 |
| * | Open notation for declaring record instances. | msozeau | 2008-10-23 |
| * | Uniformisation du format des messages d'erreur (commencent par une | herbelin | 2008-07-17 |
| * | - Patch sur "intros until 0" | herbelin | 2008-06-08 |
| * | - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait des | herbelin | 2008-05-10 |
| * | - Second pass on implementation of let pattern. Parse "let ' par [as x]? | msozeau | 2008-03-28 |
| * | Petite modif pour pouvoir faire "intros until 0" qui introduit autant |  aspiwack | 2008-02-29 |
| * | Finish let| implementation and document it | msozeau | 2008-01-31 |
| * | bug in accessing n-th abstraction | barras | 2008-01-18 |
| * | Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b... | msozeau | 2008-01-17 |
| * | 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 |
| * | Factorisation des opérations sur le type option de Util dans un module | aspiwack | 2007-12-05 |
| * | Prise en compte des notations "alias" dans la globalisation des coercions. | herbelin | 2007-11-08 |
| * | - Fixing bug 1703 ("intros until n" falls back on the variable name when | herbelin | 2007-09-21 |
| * | Correction bug sur factorisation affichage paramètres (cf r9918) | herbelin | 2007-06-30 |
| * | Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Record | herbelin | 2007-06-30 |
| * | Correction d'un bug dans l'affichage du message d'erreur real_clean | herbelin | 2007-05-29 |
| * | Add a parameter to QuestionMark evar kind to say it can be turned into an obl... | msozeau | 2007-03-19 |
| * | Add functionality to permit printing terms with references to anonymous varia... | msozeau | 2007-02-16 |
| * | correction d'un bug d'efficacite dans le printer |  jforest | 2007-01-26 |
| * | Évitement des noms de constructeurs dans les motifs de filtrage de "match" | herbelin | 2006-12-09 |
| * | The "clean integration of subtac" patch. | msozeau | 2006-05-29 |
| * | Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort | herbelin | 2006-05-19 |
| * | - 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 |
| * | - Utilisation d'abbréviations pour les types intervenant dans RCases | herbelin | 2006-04-26 |
| * | Si un fixpoint a plusieurs arguments, mais un seul de type inductif, | letouzey | 2006-04-14 |
| * | Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}. | msozeau | 2006-03-13 |
| * | Version préliminaire d'inversion de la compilation du filtrage | herbelin | 2006-01-16 |
| * | Standardisation du nom de subst_raw en subst_rawconstr | herbelin | 2006-01-11 |
| * | Restructuration et simplification des fonctions d'affichage, de détypage | herbelin | 2006-01-11 |
glondu
letouzey
herbelin
barras
soubiran
msozeau
aspiwack
jforest