coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Removing dead code in Compat.	Pierre-Marie Pédrot	2016-05-10
*	Remove dead registering code in Pcoq.	Pierre-Marie Pédrot	2016-04-24
*	Moving the Tactic Notation entry parser from Pcoq to Tacentries.	Pierre-Marie Pédrot	2016-03-31
*	Moving the Ltac definition command to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
*	Moving the proof mode parsing management to Pcoq.	Pierre-Marie Pédrot	2016-03-19
*	Do not export entry_key from Pcoq anymore.	Pierre-Marie Pédrot	2016-03-19
*	Simplifying the code of Entry.	Pierre-Marie Pédrot	2016-03-19
*	Removing dead code in Pcoq.	Pierre-Marie Pédrot	2016-03-18
*	ARGUMENT EXTEND made of only one entry share the same grammar.	Pierre-Marie Pédrot	2016-03-18
*	Removing the special status of generic arguments defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
*	Adding a universe argument to Pcoq.create_generic_entry.	Pierre-Marie Pédrot	2016-03-17
*	Relying on parsing rules rather than genarg to check if an argument is empty.	Pierre-Marie Pédrot	2016-03-17
*	Removing a source of type-unsafeness in Pcoq.	Pierre-Marie Pédrot	2016-02-02
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\
\| *	Implement support for universe binder lists in Instance and Program Fixpoint/...	Matthieu Sozeau	2016-01-23
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Removing dynamic entries from Pcoq.	Pierre-Marie Pédrot	2016-01-17
* \|	ML extensions use untyped representation of user entries.	Pierre-Marie Pédrot	2016-01-17
* \|	Removing the special status of open_constr generic argument.	Pierre-Marie Pédrot	2015-12-28
* \|	CLEANUP: Vernacexpr.VernacDeclareTacticDefinition	Matej Kosik	2015-12-18
* \|	Adding a token "index" representing positions (1st, 2nd, etc.).	Hugo Herbelin	2015-12-15
* \|	Fixing the return type of the Atoken symbol.	Pierre-Marie Pédrot	2015-10-28
* \|	Removing unused code in Pcoq.	Pierre-Marie Pédrot	2015-10-27
* \|	Finer type for Pcoq.interp_entry_name.	Pierre-Marie Pédrot	2015-10-27
* \|	Indexing existentially quantified entries returned by interp_entry_name.	Pierre-Marie Pédrot	2015-10-27
* \|	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