| Age | Commit message (Expand) | Author |
| 2012-10-16 | Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp | letouzey |
| 2012-05-29 | place all pretty-printing files in new dir printing/ | letouzey |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | Strongly reduce the dependencies of grammar.cma, modulo two hacks | letouzey |
| 2012-04-12 | lib directory is cut in 2 cma. | pboutill |
| 2012-04-06 | Removing Dhyp from debugger. | herbelin |
| 2012-03-14 | Everything compiles again. | msozeau |
| 2012-02-01 | Debugger vs tracer: Two different behaviors wrt printing: The debugger | herbelin |
| 2011-10-15 | dev/base_include: display a nice message at the end of the load | letouzey |
| 2011-04-26 | dev/base_include: no more mod_self_id | letouzey |
| 2011-04-13 | - Remove create_evar_defs | msozeau |
| 2011-04-06 | Fix dev/base_include after change of constant_body | letouzey |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-12-23 | Change of nomenclature: rawconstr -> glob_constr | glondu |
| 2010-06-18 | Quick fix for having clenv debug printer working in trunk. | herbelin |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
| 2009-11-08 | Fixed "Scheme Equality" when another instance of the scheme on the | herbelin |
| 2009-11-08 | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin |
| 2009-08-07 | Fixed incorrect optimization in Prettyp.pr_located_qualid introduced | herbelin |
| 2009-04-25 | - Fixing #2090 (occur check missing when trying to solve evar-evar equation). | herbelin |
| 2009-01-19 | - Structuring Numbers and fixing Setoid in stdlib's doc. | herbelin |
| 2008-09-02 | Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about | herbelin |
| 2008-06-08 | - Extension de "generalize" en "generalize c as id at occs". | herbelin |
| 2008-04-24 | - Add pretty-printers for Idpred, Cpred and transparent_state, used for | msozeau |
| 2008-04-23 | Prise en compte des coercions dans les clauses "with" même si le type | herbelin |
| 2008-04-13 | Bugs, nettoyage, et améliorations diverses | herbelin |
| 2007-12-07 | Ocaml toplevel convenience. | glondu |
| 2007-08-22 | - Correction bug dans syntaxe des match (liste de motifs vide était acceptée) | herbelin |
| 2007-01-19 | Export de l'afficheur de substitutions de noms de modules pour le débogueur | herbelin |
| 2006-05-23 | PÃréouverture de la plupart des fichis pour éviter d'avoir à qualifier | herbelin |
| 2006-01-29 | Ajout printer Idset.t | herbelin |
| 2006-01-11 | Restructuration et simplification des fonctions d'affichage, de détypage | herbelin |
| 2006-01-04 | Affichage concis des locations (si jamais ppterm/pprawterm sont débranchés) | herbelin |
| 2005-12-23 | MAJ restructuration constrintern.ml | herbelin |
| 2005-02-18 | Ajout constant printer | herbelin |
| 2005-01-02 | Découpage des printers pour ne pas avoir de dépendances en la vm dans les p... | herbelin |
| 2004-12-29 | Ajout printer bigint | herbelin |
| 2004-11-12 | Changement dans les boxed values . | gregoire |
| 2004-10-20 | COMMITED BYTECODE COMPILER | barras |
| 2003-04-07 | Ajout translate | herbelin |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-08-02 | Modules dans COQ\!\!\!\! | coq |
| 2002-02-15 | petits changements cosmetiques sur les tactiques | barras |
| 2001-08-10 | Parsing | herbelin |
| 2001-05-23 | amelioration des messages d'erreurs vis a vis des evars | barras |
| 2001-05-15 | Modification pour passage p-automates | mohring |
| 2001-05-10 | ajout d'un afficher de contexte et d'une fonction constbody_of_string | letouzey |
| 2001-04-03 | Make sure that the COQTOP variable is really used, when it is set. | bertot |
| 2000-12-15 | Printer | mohring |