aboutsummaryrefslogtreecommitdiff
path: root/parsing/pcoq.ml4
AgeCommit message (Expand)Author
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Migrate the grammar entry about "Ltac" into g_vernac.ml4.letouzey
2012-03-02Noise for nothingpboutill
2012-01-20Reverted previous commit, which broke library compilation.ppedrot
2012-01-20This is a quick hack to permit the parsing of the locality flag in the Progra...ppedrot
2011-07-27Oversight in revision 14292.pboutill
2011-04-26Pcoq.ml4: fix a typo in a comment to please ocamldocletouzey
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-11-18adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6letouzey
2010-11-16Support for camlp5 6.02.0 (Closes: #2432)glondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-07-22Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).herbelin
2010-06-08Using vernac parsing for Functionjforest
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-19Nicer representation of tokens, more independant of camlp*letouzey
2010-05-19static (and shared) camlp4use instead of per-file declarationletouzey
2010-05-19Discontinue support for ocaml 3.09.*letouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-05-27=?utf-8?q?D=C3=A9sinterdiction=20de=20GDELETE=5FRULE=20dans=20pcoq.ml4.=20Mal...aspiwack
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-04-08- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingherbelin
2009-01-19- Structuring Numbers and fixing Setoid in stdlib's doc.herbelin
2009-01-14Fixing/improving management of uniform prefix Local and Globalherbelin
2008-11-09More factorization of inductive/record and typeclasses: move classmsozeau
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-07-11Correction d'un autre bug autour de la gestion des niveaux vides deherbelin
2008-05-26Résolution bug #1850 sur notations avec niveaux inconnus deherbelin
2008-05-11- Cleanup parsing of binders, reducing to a single production for allmsozeau
2008-05-08** Efficacité, bugs, robustesse CoqIDE **herbelin
2008-04-30Contournement laborieux de la "feature" de camlp5 qui entrainait leherbelin
2008-04-26Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour herbelin
2008-03-06Syntax changes in typeclasses, remove "?" for usual implicit argumentsmsozeau
2008-01-15Generalize instance declarations to any context, better name handling. Add ho...msozeau
2008-01-07Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...msozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-09-28Creation of a new token PATTERNIDENT (?ident) for intro patterns, soglondu
2007-09-15* Adding compability with ocaml 3.10 + camlp5 (rework of letouzey
2007-07-16Generalized CAMLP4USE for pp dependenciescorbinea
2007-04-11Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y aherbelin