| Age | Commit message (Expand) | Author |
|---|
| 2012-12-14 | Modulification of dir_path | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-10-04 | Moved Compat to parsing. This permits to break the dependency of the | ppedrot |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-05-29 | remove many excessive open Util & Errors in mli's | letouzey |
| 2012-05-29 | Migrate the grammar entry about "Ltac" into g_vernac.ml4. | letouzey |
| 2012-05-29 | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey |
| 2012-05-29 | Glob_term now mli-only, operations now in Glob_ops | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-01-20 | Reverted previous commit, which broke library compilation. | ppedrot |
| 2012-01-20 | This is a quick hack to permit the parsing of the locality flag in the Progra... | ppedrot |
| 2010-12-24 | More {raw => glob} changes for consistency | glondu |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-07-22 | Extension of the recursive notations mechanism | herbelin |
| 2010-07-22 | Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt). | herbelin |
| 2010-06-22 | New script dev/tools/change-header to automatically update Coq files headers. | herbelin |
| 2010-06-08 | Using vernac parsing for Function | jforest |
| 2010-05-19 | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey |
| 2010-05-19 | Nicer representation of tokens, more independant of camlp* | letouzey |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-29 | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2010-03-29 | Several bug-fixes and improvements of coqdoc | herbelin |
| 2010-01-07 | Include can accept both Module and Module Type | letouzey |
| 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-09-11 | Generalized the possibility to refer to a global name by a notation | herbelin |
| 2009-04-27 | - Fixed a little bug in previous commit (bad failure in case of unknown entry). | herbelin |
| 2009-04-27 | - Cleaning (unification of ML names, removal of obsolete code, | herbelin |
| 2009-04-25 | - Fixing #2090 (occur check missing when trying to solve evar-evar equation). | herbelin |
| 2009-01-14 | Fixing/improving management of uniform prefix Local and Global | herbelin |
| 2008-11-09 | More factorization of inductive/record and typeclasses: move class | msozeau |
| 2008-10-22 | A much better implementation of implicit generalization: | msozeau |
| 2008-10-19 | - Export de pattern_ident vers les ARGUMENT EXTEND and co. | herbelin |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-07-11 | Correction d'un autre bug autour de la gestion des niveaux vides de | herbelin |
| 2008-07-07 | - Improve [Context] vernacular to allow arbitrary binders, not just | msozeau |
| 2008-07-04 | Fixes in handling of implicit arguments: | msozeau |
| 2008-05-26 | Résolution bug #1850 sur notations avec niveaux inconnus de | herbelin |
| 2008-05-11 | - Cleanup parsing of binders, reducing to a single production for all | msozeau |
| 2008-05-06 | Postpone the search for the recursive argument index from the user given | msozeau |
| 2008-04-30 | Contournement laborieux de la "feature" de camlp5 qui entrainait le | herbelin |
| 2008-04-26 | Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour | herbelin |
| 2008-03-06 | Syntax changes in typeclasses, remove "?" for usual implicit arguments | msozeau |
| 2008-01-15 | Generalize instance declarations to any context, better name handling. Add ho... | msozeau |
| 2008-01-07 | Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp... | msozeau |
