coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	Type-safe grammar extensions.	Pierre-Marie Pédrot	2015-10-27
* \|	Pcoq entries are given a proper module.	Pierre-Marie Pédrot	2015-10-26
* \|	Getting rid of the Atactic entry.	Pierre-Marie Pédrot	2015-10-25
* \|	Getting rid of the Agram entry.	Pierre-Marie Pédrot	2015-10-25
* \|	Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.	Pierre-Marie Pédrot	2015-10-21
* \|	Expliciting some uses of Compat module.	Pierre-Marie Pédrot	2015-10-21
\|/
*	grammar: export constr_eval	Enrico Tassi	2015-03-30
*	grammar: export hypident	Enrico Tassi	2015-03-30
*	Update headers.	Maxime Dénès	2015-01-12
*	Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels)	Hugo Herbelin	2014-11-06
*	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin	2014-08-18
*	Moving the TacExtend node from atomic to plain tactics.	Pierre-Marie Pédrot	2014-08-18
*	Properly declare uconstr as an argument for TACTIC EXTEND.	Arnaud Spiwack	2014-08-05
*	Removing useless use of metaids in tactic AST.	Pierre-Marie Pédrot	2014-05-22
*	Adding way to get the list of the accepted tactic notation arguments.	Pierre-Marie Pédrot	2014-05-17
*	Closing bug #3260	Julien Forest	2014-04-14
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Removing non-marshallable data from the Agram constructor. Instead of	Pierre-Marie Pédrot	2014-02-16
*	Getting rid of casted_open_constr. It was only used by the	Pierre-Marie Pédrot	2013-11-30
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
*	Updating headers.	herbelin	2012-08-08
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
*	Migrate the grammar entry about "Ltac" into g_vernac.ml4.	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Noise for nothing	pboutill	2012-03-02
*	Reverted previous commit, which broke library compilation.	ppedrot	2012-01-20
*	This is a quick hack to permit the parsing of the locality flag in the Progra...	ppedrot	2012-01-20
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).	herbelin	2010-07-22
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Using vernac parsing for Function	jforest	2010-06-08
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
*	Nicer representation of tokens, more independant of camlp*	letouzey	2010-05-19
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29
*	Include can accept both Module and Module Type	letouzey	2010-01-07
*	In "simpl c" and "change c with d", c can be a pattern.	herbelin	2009-12-24