aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.ml4
Commit message (Expand)AuthorAge
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Migrate the grammar entry about "Ltac" into g_vernac.ml4.Gravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Reverted previous commit, which broke library compilation.Gravatar ppedrot2012-01-20
* This is a quick hack to permit the parsing of the locality flag in the Progra...Gravatar ppedrot2012-01-20
* Oversight in revision 14292.Gravatar pboutill2011-07-27
* Pcoq.ml4: fix a typo in a comment to please ocamldocGravatar letouzey2011-04-26
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6Gravatar letouzey2010-11-18
* Support for camlp5 6.02.0 (Closes: #2432)Gravatar glondu2010-11-16
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).Gravatar herbelin2010-07-22
* Using vernac parsing for FunctionGravatar jforest2010-06-08
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Nicer representation of tokens, more independant of camlp*Gravatar letouzey2010-05-19
* static (and shared) camlp4use instead of per-file declarationGravatar letouzey2010-05-19
* Discontinue support for ocaml 3.09.*Gravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* =?utf-8?q?D=C3=A9sinterdiction=20de=20GDELETE=5FRULE=20dans=20pcoq.ml4.=20Mal...Gravatar aspiwack2009-05-27
* - Fixed a little bug in previous commit (bad failure in case of unknown entry).Gravatar herbelin2009-04-27
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* - Fixing #2090 (occur check missing when trying to solve evar-evar equation).Gravatar herbelin2009-04-25
* - Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingGravatar herbelin2009-04-08
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* Fixing/improving management of uniform prefix Local and GlobalGravatar herbelin2009-01-14
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Correction d'un autre bug autour de la gestion des niveaux vides deGravatar herbelin2008-07-11
* Résolution bug #1850 sur notations avec niveaux inconnus deGravatar herbelin2008-05-26
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* ** Efficacité, bugs, robustesse CoqIDE **Gravatar herbelin2008-05-08
* Contournement laborieux de la "feature" de camlp5 qui entrainait leGravatar herbelin2008-04-30
* Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour Gravatar herbelin2008-04-26
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* Generalize instance declarations to any context, better name handling. Add ho...Gravatar msozeau2008-01-15
* Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...Gravatar msozeau2008-01-07
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Creation of a new token PATTERNIDENT (?ident) for intro patterns, soGravatar glondu2007-09-28
* * Adding compability with ocaml 3.10 + camlp5 (rework of Gravatar letouzey2007-09-15
* Generalized CAMLP4USE for pp dependenciesGravatar corbinea2007-07-16
* Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y aGravatar herbelin2007-04-11