coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-07-02	Moving various ml4 files to mlg.	Pierre-Marie Pédrot

2018-02-27	Update headers following #6543.	Théo Zimmermann

2018-02-17	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle
	longer use camlp4.
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2017-02-17	Moving the Ltac plugin to a pack-based one.	Pierre-Marie Pédrot
	This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements.
2016-01-20	Update copyright headers.	Maxime Dénès

2015-01-12	Update headers.	Maxime Dénès

2014-05-12	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot
	corresponding Declare ML Module command. This changes essentially two things: 1. ML plugins are forced to use the DECLARE PLUGIN statement before any TACTIC EXTEND statement. The plugin name must be exactly the string passed to the Declare ML Module command. 2. ML tactics are only made available after the Coq module that does the corresponding Declare ML Module is imported. This may break a few things, as it already broke quite some uses of omega in the stdlib.
2012-08-08	Updating headers.	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29	place all files specific to camlp4 syntax extensions in grammar/	letouzey
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15387 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-13	Added a Btauto plugin, that solves boolean tautologies.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14897 85f007b7-540e-0410-9357-904b9bb8a0f7