| Commit message (Expand) | Author | Age |
* | Two adaptations after the changes of level of -> | letouzey | 2012-07-06 |
* | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey | 2012-05-29 |
* | Migrate the grammar entry about "Ltac" into g_vernac.ml4. | letouzey | 2012-05-29 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | 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 | 2012-01-20 |
* | Oversight in revision 14292. | pboutill | 2011-07-27 |
* | Pcoq.ml4: fix a typo in a comment to please ocamldoc | letouzey | 2011-04-26 |
* | Rename rawterm.ml into glob_term.ml | glondu | 2010-12-23 |
* | adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6 | letouzey | 2010-11-18 |
* | Support for camlp5 6.02.0 (Closes: #2432) | glondu | 2010-11-16 |
* | 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 |
* | 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 |
* | static (and shared) camlp4use instead of per-file declaration | letouzey | 2010-05-19 |
* | Discontinue support for ocaml 3.09.* | letouzey | 2010-05-19 |
* | Remove the svn-specific $Id$ annotations | letouzey | 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 |
* | 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 |
* | =?utf-8?q?D=C3=A9sinterdiction=20de=20GDELETE=5FRULE=20dans=20pcoq.ml4.=20Mal... | aspiwack | 2009-05-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-27 |
* | - Fixing #2090 (occur check missing when trying to solve evar-evar equation). | herbelin | 2009-04-25 |
* | - Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing | herbelin | 2009-04-08 |
* | - Structuring Numbers and fixing Setoid in stdlib's doc. | herbelin | 2009-01-19 |
* | 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 |
* | - Export de pattern_ident vers les ARGUMENT EXTEND and co. | herbelin | 2008-10-19 |
* | Uniformisation du format des messages d'erreur (commencent par une | herbelin | 2008-07-17 |
* | Correction d'un autre bug autour de la gestion des niveaux vides de | herbelin | 2008-07-11 |
* | 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 |
* | ** Efficacité, bugs, robustesse CoqIDE ** | herbelin | 2008-05-08 |
* | 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 |
* | Plus de combinateurs sont passés de Util à Option. Le module Options | aspiwack | 2007-12-06 |
* | Factorisation des opérations sur le type option de Util dans un module | aspiwack | 2007-12-05 |
* | 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 |
* | Generalized CAMLP4USE for pp dependencies | corbinea | 2007-07-16 |