aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.ml4
Commit message (Expand)AuthorAge
* Properly declare uconstr as an argument for TACTIC EXTEND.Gravatar Arnaud Spiwack2014-08-05
* Fixing #3390 (mismatch simple_tactic/tactic0 leading to segfault).Gravatar Hugo Herbelin2014-06-21
* Adding way to get the list of the accepted tactic notation arguments.Gravatar Pierre-Marie Pédrot2014-05-17
* Closing bug #3260Gravatar Julien Forest2014-04-14
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Removing non-marshallable data from the Agram constructor. Instead ofGravatar Pierre-Marie Pédrot2014-02-16
* Removing the useless pattern ident genarg.Gravatar Pierre-Marie Pédrot2013-12-19
* Getting rid of casted_open_constr. It was only used by theGravatar Pierre-Marie Pédrot2013-11-30
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Expurgating the useless difference between List0 and List1 at theGravatar ppedrot2013-07-05
* Removing the use of leveled tactics wit_tacticn. It is now handledGravatar ppedrot2013-07-02
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Proof-of-concept: moved four easy-to-handle generic arguments toGravatar ppedrot2013-06-18
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
* avoid (Int.equal (cmp ...) 0) when a boolean equality existsGravatar letouzey2013-02-19
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Monomorphization (parsing)Gravatar ppedrot2012-11-25
* More monomorphizationsGravatar ppedrot2012-11-13
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Two adaptations after the changes of level of ->Gravatar letouzey2012-07-06
* 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