| Age | Commit message (Expand) | Author |
|---|
| 2009-12-24 | In "simpl c" and "change c with d", c can be a pattern. | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-03-28 | Rewrite of Program Fixpoint to overcome the previous limitations: | msozeau |
| 2008-11-05 | Move Record desugaring to constrintern and add ability to use notations | msozeau |
| 2008-10-23 | Open notation for declaring record instances. | msozeau |
| 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-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-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-21 | Compatibilité ocamlweb pour cible doc | herbelin |
| 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-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 |
