| 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 |
| * | 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 |
| * | Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt). | herbelin | 2010-07-22 |
| * | New script dev/tools/change-header to automatically update Coq files headers. | herbelin | 2010-06-22 |
| * | Using vernac parsing for Function |  jforest | 2010-06-08 |
| * | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey | 2010-05-19 |
| * | Nicer representation of tokens, more independant of camlp* | letouzey | 2010-05-19 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | Move from ocamlweb to ocamdoc to generate mli documentation |  pboutill | 2010-04-29 |
| * | Here comes the commit, announced long ago, of the new tactic engine. |  aspiwack | 2010-04-22 |
| * | Several bug-fixes and improvements of coqdoc | herbelin | 2010-03-29 |
| * | Include can accept both Module and Module Type | letouzey | 2010-01-07 |
| * | In "simpl c" and "change c with d", c can be a pattern. | herbelin | 2009-12-24 |
| * | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
| * | Generalized the possibility to refer to a global name by a notation | herbelin | 2009-09-11 |
| * | - 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-27 |
| * | - Fixing #2090 (occur check missing when trying to solve evar-evar equation). | herbelin | 2009-04-25 |
| * | Fixing/improving management of uniform prefix Local and Global | herbelin | 2009-01-14 |
| * | More factorization of inductive/record and typeclasses: move class |  msozeau | 2008-11-09 |
| * | A much better implementation of implicit generalization: | msozeau | 2008-10-22 |
| * | - Export de pattern_ident vers les ARGUMENT EXTEND and co. | herbelin | 2008-10-19 |
| * | Évolutions diverses et variées. | herbelin | 2008-08-04 |
| * | Correction d'un autre bug autour de la gestion des niveaux vides de | herbelin | 2008-07-11 |
| * | - Improve [Context] vernacular to allow arbitrary binders, not just | msozeau | 2008-07-07 |
| * | Fixes in handling of implicit arguments: | msozeau | 2008-07-04 |
| * | Résolution bug #1850 sur notations avec niveaux inconnus de | herbelin | 2008-05-26 |
| * | - Cleanup parsing of binders, reducing to a single production for all | msozeau | 2008-05-11 |
| * | Postpone the search for the recursive argument index from the user given | msozeau | 2008-05-06 |
| * | Contournement laborieux de la "feature" de camlp5 qui entrainait le | herbelin | 2008-04-30 |
| * | Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour | herbelin | 2008-04-26 |
| * | Syntax changes in typeclasses, remove "?" for usual implicit arguments | msozeau | 2008-03-06 |
| * | Generalize instance declarations to any context, better name handling. Add ho... | msozeau | 2008-01-15 |
| * | Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp... | msozeau | 2008-01-07 |
| * | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau | 2007-12-31 |
| * | Creation of a new token PATTERNIDENT (?ident) for intro patterns, so | glondu | 2007-09-28 |
| * | * Adding compability with ocaml 3.10 + camlp5 (rework of | letouzey | 2007-09-15 |
| * | Ajout de la possibilité de faire référence dans certains cas à un nom | herbelin | 2007-04-28 |
| * | Suppression du type 'tac dans les abstract_argument_type: devenu inutile | herbelin | 2006-11-20 |
| * | gestion speciale du niveau 5 des ltac |  barras | 2006-11-02 |
| * | Declarative Proof Language: main commit |  corbinea | 2006-09-20 |
| * | Changement du type d'argument 'TacticArgType X' en un type | herbelin | 2006-06-08 |
| * | Correction trou de subject-reduction de create_arg dans genarg.mli | herbelin | 2006-06-07 |
| * | Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement... | herbelin | 2006-01-09 |
| * | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin | 2005-12-26 |
| * | Added entry constr_may_eval for tactic extensions (new syntax) | herbelin | 2005-06-22 |
| * | Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux... | herbelin | 2005-05-17 |
glondu
letouzey
herbelin
jforest
pboutill
aspiwack
msozeau
barras
corbinea