coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Moving the TacExtend node from atomic to plain tactics.	Pierre-Marie Pédrot	2014-08-18
\| \| \| \| \|	Also taking advantage of the change to rename it into TacML. Ultimately should allow ML tactic to return values.
*	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot	2014-07-27
\| \| \| \|	potentially conflicting tactics names from different plugins.
*	Moving the ML tactic extension mechanism to a Libobject-based one.	Pierre-Marie Pédrot	2014-05-12
\|
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
\| \| \| \| \| \| \| \|	With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-10
\| \| \| \| \| \| \| \| \|	Instead of putting the body directly in the AST, we register it in a table. This time it should work properly. Tactic notation are given kernel names to ensure the unicity of their contents. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17079 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revert the previous commit. It broke Coq compilation.	ppedrot	2013-11-09
\| \| \| \| \| \| \| \|	Tactics notation interpretation was messed up because of the use of identical keys for different notations. All my tentative fixes were unsuccessful, so better blankly revert the commit for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17078 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-09
\| \| \| \| \| \|	Instead of putting the body directly in the AST, we register it in a table. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17077 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Moving notation types into grammar rule.	ppedrot	2013-11-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17076 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaning and documenting Egramcoq.	ppedrot	2013-11-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17075 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a generic handler of Ltac quotations, based on the existing	ppedrot	2013-06-27
\| \| \| \| \| \| \| \| \| \| \|	syntax constr:foo and ipattern:bar (which is not very nice for parsing, b.t.w.). Now one is able to dynamically add quotations of the form name:... that will use the provided function to create a dynamically typed argument. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16611 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Dir_path --> DirPath	letouzey	2013-02-19
\| \| \| \| \| \| \| \|	Ok, this is merely a matter of taste, but up to now the usage in Coq is rather to use capital letters instead of _ in the names of inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modulification of dir_path	ppedrot	2012-12-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modulification of identifier	ppedrot	2012-12-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding a nominal typing layer to Metasyntax in order to clarify	ppedrot	2012-10-04
\| \| \| \| \| \| \| \|	things up. Records are used instead of their equivalents as tuples. This is maybe syntactically heavier, but this is semantically equivalent and easier to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15848 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
\| \| \| \| \| \| \| \| \| \| \| \|	kernel on CAMLP4/5 structures, and consequently should also erase such structures from vo files. This modification requires some code duplication, mainly while reimplementing our own location data type. This is chiefly visible in the ml4 files, where CAMLP4/5 locations must be manually converted to our locations with an explicit (!@) cast operator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Split Egrammar into Egramml and Egramcoq	letouzey	2012-05-29
	Two gains: - no Summary in Grammar.cma - get rid of the hack concerning error_invalid_pattern_notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15386 85f007b7-540e-0410-9357-904b9bb8a0f7