coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	CLEANUP: removing unused field	Matej Kosik	2016-01-11
*	merge	Matej Kosik	2016-01-11
\|\
\| *	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \|	COMMENTS: of "Constr.case_info" type were updated.	Matej Kosik	2016-01-11
* \|	COMMENTS: added to the "Names.inductive" and "Names.constructor" types.	Matej Kosik	2016-01-11
* \|	Fix bug 4479: "Error: Rewriting base foo does not exist." should be catchable.	Pierre-Marie Pédrot	2016-01-09
* \|	Monotonizing Ftactic.	Pierre-Marie Pédrot	2016-01-08
* \|	Remove deprecated command-line options such as "-as".	Guillaume Melquiond	2016-01-06
* \|	Make code more readable by not mixing list traversal and option processing.	Guillaume Melquiond	2016-01-06
* \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-06
\|\ \
\| * \|	Prevent coq_makefile from parsing project files in the reverse order. (Fix bu...	Guillaume Melquiond	2016-01-06
\| * \|	Protect code against changes in Map interface.	Maxime Dénès	2016-01-06
\| * \|	Disable warning 31 when generating coqtop from coqmktop.	Maxime Dénès	2016-01-05
* \| \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-05
\|\ \ \
\| \| * \|	Avoid warning 31: test printer was linked twice with Dynlink and Str.	Maxime Dénès	2016-01-05
\| \| * \|	Fix order of files in mllib.	Maxime Dénès	2016-01-05
\| \|/ /
\| * \|	COMMENTS: Predicate	Matej Kosik	2016-01-05
\| * \|	fixup d2b468a, evar normalization is needed	Enrico Tassi	2016-01-04
\| * \|	Extraction: msg_notice instead of msg_info.	Pierre Courtieu	2016-01-04
\| * \|	Fix handling of side-effects in case of `Opaque side-effects as well.	Matthieu Sozeau	2016-01-04
\| * \|	par: check if the goal is not ground and fail (fix #4465)	Enrico Tassi	2016-01-04
\| * \|	workers: purge short version of -load-vernac too (fix #4458)	Enrico Tassi	2016-01-04
* \| \|	Use streams rather than strings to handle bullet suggestions.	Guillaume Melquiond	2016-01-02
* \| \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \| \|	Remove keys for evar and meta, since they cannot occur.	Guillaume Melquiond	2016-01-02
* \| \|	Remove some useless type declarations.	Guillaume Melquiond	2016-01-02
* \| \|	Remove some useless module opening.	Guillaume Melquiond	2016-01-02
* \| \|	Remove duplicate definition.	Guillaume Melquiond	2016-01-02
* \| \|	Remove duplicate declarations.	Guillaume Melquiond	2016-01-02
* \| \|	Reduce dependencies of interface files.	Guillaume Melquiond	2016-01-02
* \| \|	Avoid warnings about loop indices.	Guillaume Melquiond	2016-01-02
* \| \|	Remove useless rec flags.	Guillaume Melquiond	2016-01-02
* \| \|	Simplification of grammar_prod_item type.	Pierre-Marie Pédrot	2016-01-02
* \| \|	Proper datatype for EXTEND syntax tokens.	Pierre-Marie Pédrot	2016-01-02
* \| \|	Separation of concern in TacAlias API.	Pierre-Marie Pédrot	2016-01-02
* \| \|	Fix typos.	Guillaume Melquiond	2016-01-01
* \| \|	Remove unused hashconsing code.	Guillaume Melquiond	2016-01-01
* \| \|	Do not make it harder on the compiler optimizer by packing arguments.	Guillaume Melquiond	2016-01-01
* \| \|	Remove unused functions.	Guillaume Melquiond	2016-01-01
* \| \|	Remove unplugged button from the interface.	Guillaume Melquiond	2016-01-01
* \| \|	Remove useless recursive flags.	Guillaume Melquiond	2016-01-01
* \| \|	Remove unused open.	Guillaume Melquiond	2016-01-01
* \| \|	Remove duplicate declarations.	Guillaume Melquiond	2016-01-01
\| * \|	Put implicits back as in 8.4.	Matthieu Sozeau	2015-12-31
\| * \|	Fix bug #4456, anomaly in handle-side effects	Matthieu Sozeau	2015-12-31
* \| \|	Remove unused function Checker.print_loc.	Guillaume Melquiond	2015-12-31
* \| \|	Merge branch 'v8.5' into trunk	Guillaume Melquiond	2015-12-31
\|\\| \|
* \| \|	Do not compose List.length with List.filter.	Guillaume Melquiond	2015-12-31
* \| \|	Remove Library.mem, which is pointless since 8.5.	Guillaume Melquiond	2015-12-31
\| * \|	Do not dump a glob reference when its location is ghost. (Fix bug #4469)	Guillaume Melquiond	2015-12-31