aboutsummaryrefslogtreecommitdiff
path: root/parsing/pcoq.ml4
AgeCommit message (Expand)Author
2015-10-21Turn Pcoq into a regular ML file.Pierre-Marie Pédrot
2015-10-21Expanding the grammar extensions of Pcoq.Pierre-Marie Pédrot
2015-10-21Removing the dependencies of Pcoq in IFDEF macros.Pierre-Marie Pédrot
2015-10-14Fix some typos.Guillaume Melquiond
2015-07-01Notation: use same level for "@" in constr: and pattern: (Close: #4272)Enrico Tassi
2015-03-30grammar: export constr_evalEnrico Tassi
2015-03-30grammar: export hypidentEnrico Tassi
2015-01-12Update headers.Maxime Dénès
2014-11-06Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels)Hugo Herbelin
2014-08-05Properly declare uconstr as an argument for TACTIC EXTEND.Arnaud Spiwack
2014-06-21Fixing #3390 (mismatch simple_tactic/tactic0 leading to segfault).Hugo Herbelin
2014-05-17Adding way to get the list of the accepted tactic notation arguments.Pierre-Marie Pédrot
2014-04-14Closing bug #3260Julien Forest
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-16Removing non-marshallable data from the Agram constructor. Instead ofPierre-Marie Pédrot
2013-12-19Removing the useless pattern ident genarg.Pierre-Marie Pédrot
2013-11-30Getting rid of casted_open_constr. It was only used by thePierre-Marie Pédrot
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-07-05Expurgating the useless difference between List0 and List1 at theppedrot
2013-07-02Removing the use of leveled tactics wit_tacticn. It is now handledppedrot
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
2013-06-18Proof-of-concept: moved four easy-to-handle generic arguments toppedrot
2013-06-06Uniformizing generic argument types.ppedrot
2013-02-19avoid (Int.equal (cmp ...) 0) when a boolean equality existsletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-11-25Monomorphization (parsing)ppedrot
2012-11-13More monomorphizationsppedrot
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-17More cleaning on Utils and CList. Some parts of the code beingppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-08-08Updating headers.herbelin
2012-07-06Two adaptations after the changes of level of ->letouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 21:00:53 +0000