coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	Properly handle the only printing flag in Reserved Notations.	Pierre-Marie Pédrot	2016-06-28
*	Properly handling the only printing flag when parsing rules already exist.	Pierre-Marie Pédrot	2016-06-28
*	[feedback] Add optional ?loc parameter to loggers.	Emilio Jesus Gallego Arias	2016-06-25
*	Merge remote-tracking branch 'github/pr/194' into trunk	Maxime Dénès	2016-06-16
\|\
* \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-13
\|\ \
\| * \|	Tentatively fixing misguiding error message with "binder" type in	Hugo Herbelin	2016-06-13
\| \| *	Adding an only printing flag to notations.	Pierre-Marie Pédrot	2016-06-07
\| \| *	Removing the use to Egramcoq.recover_constr_grammar.	Pierre-Marie Pédrot	2016-06-07
\| \|/ \|/\|
\| *	Revert "Rename Lexer -> CLexer."	Pierre-Marie Pédrot	2016-05-31
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-09
\|\\|
\| *	Rename Lexer -> CLexer.	Pierre-Marie Pédrot	2016-05-09
* \|	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\\|
\| *	Properly handle notations containing spaces (bug #4538).	Guillaume Melquiond	2016-05-02
* \|	Revert "A heuristic to add parentheses in the presence of rules such as"	Hugo Herbelin	2016-04-27
* \|	A heuristic to add parentheses in the presence of rules such as	Hugo Herbelin	2016-04-27
* \|	Was too restrictive in syntactic definitions, not imagining that they	Hugo Herbelin	2016-03-28
* \|	Moving the tactic related code from Metasyntax to a new file.	Pierre-Marie Pédrot	2016-03-20
* \|	Removing dead code in Pcoq.	Pierre-Marie Pédrot	2016-03-18
* \|	Relying on parsing rules rather than genarg to check if an argument is empty.	Pierre-Marie Pédrot	2016-03-17
* \|	Printing notations: Cleaning in anticipation of fixing #4592.	Hugo Herbelin	2016-02-28
* \|	Infering atomic ML entries from their grammar.	Pierre-Marie Pédrot	2016-02-01
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\|
\| *	Fixing bug #4495: Failed assertion in metasyntax.ml.	Pierre-Marie Pédrot	2016-01-24
* \|	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
* \|	Tactic notation printing accesses all the token data.	Pierre-Marie Pédrot	2016-01-16
* \|	Simplification of grammar_prod_item type.	Pierre-Marie Pédrot	2016-01-02
* \|	Separation of concern in TacAlias API.	Pierre-Marie Pédrot	2016-01-02
* \|	External tactics and notations now accept any tactic argument.	Pierre-Marie Pédrot	2015-12-30
* \|	Type-safe Egramml.grammar_prod_item.	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
* \|	Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.	Pierre-Marie Pédrot	2015-10-21
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-28
\|\\|
\| *	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg	2015-06-26
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	Adding a test to check whether two tactic notations conflict.	Pierre-Marie Pédrot	2015-05-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
\| *	Fixing bug #4190.	Pierre-Marie Pédrot	2015-04-16
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-03-30
\|\\|
\| *	Revert "Useless check when loading notations through import."	Pierre-Marie Pédrot	2015-03-24
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-11
\|\\|
\| *	Tactic Notation: use stable unique key for notations (Close: 3970)	Enrico Tassi	2015-02-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-10
\|\\|