| Age | Commit message (Expand) | Author |
|---|
| 2008-07-24 | broke cyclic dependencies | barras |
| 2008-06-10 | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin |
| 2008-03-28 | - Second pass on implementation of let pattern. Parse "let ' par [as x]? | msozeau |
| 2008-01-17 | Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b... | msozeau |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-12-05 | Factorisation des opérations sur le type option de Util dans un module | aspiwack |
| 2007-03-19 | Add a parameter to QuestionMark evar kind to say it can be turned into an obl... | msozeau |
| 2007-01-26 | correction d'un bug d'efficacite dans le printer | jforest |
| 2006-10-09 | Notations: | herbelin |
| 2006-06-22 | Added {measure x f} as a valid recursion order. | msozeau |
| 2006-05-30 | Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme... | herbelin |
| 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-26 | - Utilisation d'abbréviations pour les types intervenant dans RCases | herbelin |
| 2006-04-14 | Si un fixpoint a plusieurs arguments, mais un seul de type inductif, | letouzey |
| 2006-03-13 | Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}. | msozeau |
| 2006-01-08 | Fonctions de conversion rawconstr <-> cases_pattern | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-01-03 | HUGE COMMIT | sacerdot |
| 2004-12-29 | ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien... | herbelin |
| 2004-11-16 | Names.substitution (and related functions) and Term.subst_mps moved to | sacerdot |
| 2004-10-20 | COMMITED BYTECODE COMPILER | barras |
| 2004-09-15 | hiding the meta_map in evar_defs | barras |
| 2004-08-23 | Correction bug #830 : les noms des implicites temporaires étaient inconnus a... | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-07-16 | Suppression de Rawterm.loc, branchement sur Util.loc | herbelin |
| 2004-03-05 | modif des fixpoints pour que si on donne une notation au produit, les pts fix... | barras |
| 2004-02-18 | - fixed the Assert_failure error in kernel/modops | barras |
| 2003-12-19 | Substitution dans REvar et PEvar plutot que encodage via noeud application po... | herbelin |
| 2003-11-19 | Deplacement subst_rawconstr dans Rawterm | herbelin |
| 2003-09-09 | Ajout construction If primitive dans constr_expr et rawconstr | herbelin |
| 2003-08-11 | Nouvelle mouture du traducteur v7->v8 | herbelin |
| 2003-05-19 | Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern | herbelin |
| 2003-04-07 | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin |
| 2003-03-29 | Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar) | herbelin |
| 2003-03-21 | *** empty log message *** | barras |
| 2002-12-21 | Légère amélioration des messages d'erreur des with-bindings et des Rewrite | herbelin |
| 2002-12-09 | Ajout Simpl et Change sur des sous-termes | herbelin |
| 2002-11-18 | Ajout de Cases dans abbreviatable constr (aconstr) [utilisé dans la | herbelin |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-10-13 | Ajout map_rawconstr | herbelin |
| 2002-10-12 | Restriction sur la forme des Syntactic Definition et re-localisation en fonct... | herbelin |
| 2002-09-03 | pretyping/pretyping.ml | herbelin |
| 2002-08-02 | Modules dans COQ\!\!\!\! | coq |
| 2002-05-30 | Finalement un seul constr pour l'instant dans ExtraRedExpr | herbelin |
| 2002-05-29 | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin |
| 2002-04-11 | Deuxième passe sur la localisation des messages d'erreurs sur les evars non ... | herbelin |
| 2002-04-10 | Amélioration des messages d'erreurs concernant l'inférence des implicites | herbelin |
