coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Moving Autorewrite to Hightatctic.	Pierre-Marie Pédrot	2016-03-06
*	Putting Tactic_debug just below Tacinterp.	Pierre-Marie Pédrot	2016-03-06
*	Removing dependency of Himsg in tactic files.	Pierre-Marie Pédrot	2016-03-06
*	Moving Tactic_debug to tactics/ folder.	Pierre-Marie Pédrot	2016-03-06
*	Moving Ltac traces to Tacexpr and Tacinterp.	Pierre-Marie Pédrot	2016-03-06
*	Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.	Pierre-Marie Pédrot	2016-03-06
*	Removing useless grammar.cma dependencies.	Pierre-Marie Pédrot	2016-03-06
*	Splitting the nsatz ML module into an implementation and a grammar files.	Pierre-Marie Pédrot	2016-03-06
*	Moving Eauto to a simple ML file.	Pierre-Marie Pédrot	2016-03-06
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\
* \|	Using build_selector from Equality as a replacement of the selector	Hugo Herbelin	2016-03-05
* \|	Exporting build_selector, a component of discriminate, for use in congruence.	Hugo Herbelin	2016-03-05
* \|	Generalizing the uses of tactic scopes everywhere.	Pierre-Marie Pédrot	2016-03-05
\|\ \
\| \| *	Fixing bug #4608: Anomaly "output_value: abstract value (outside heap)".	Pierre-Marie Pédrot	2016-03-05
\| \| *	Fix #4607: do not read native code files if native compiler was disabled.	Maxime Dénès	2016-03-04
\| \| *	This fix is probably not enough to justify that there are no problems with	Maxime Dénès	2016-03-04
\| * \|	Adding some standard arguments in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
\| \| *	Rename Ephemeron -> CEphemeron.	Maxime Dénès	2016-03-04
\| * \|	All arguments defined through ARGUMENT EXTEND declare a tactic scope.	Pierre-Marie Pédrot	2016-03-04
\| * \|	Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].	Pierre-Marie Pédrot	2016-03-04
\| * \|	Exchanging roles of tactic_arg and tactic_top_or_arg entries.	Pierre-Marie Pédrot	2016-03-04
\| * \|	Removing the UConstr entry of the tactic_arg AST.	Pierre-Marie Pédrot	2016-03-04
\| * \|	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
\| * \|	Uniformizing the parsing of argument scopes in Ltac.	Pierre-Marie Pédrot	2016-03-04
\|/ /
* \|	Merge pull request #97 from clarus/trunk	Pierre-Marie Pédrot	2016-03-04
\|\ \
\| \| *	Fix a typo in dev/doc/changes.txt	Jason Gross	2016-03-04
\| \| *	Adding a test for the behaviour of open_constr described in #3777.	Pierre-Marie Pédrot	2016-03-03
\| \| *	Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.	Pierre-Marie Pédrot	2016-03-03
* \| \|	Merge branch 'clean-atomic-tactics'	Pierre-Marie Pédrot	2016-02-29
\|\ \ \
\| * \| \|	Moving the "move" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
\| * \| \|	Moving the "exists" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
\| * \| \|	Moving the "symmetry" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
\| * \| \|	Moving the "generalize dependent" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
\| * \| \|	Moving the "clearbody" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
\| * \| \|	Moving the "clear" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
\| * \| \|	Moving the "cofix" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
\| * \| \|	Moving the "fix" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot	2016-02-29
\|/ / /
* \| \|	Printing notations: Cleaning in anticipation of fixing #4592.	Hugo Herbelin	2016-02-28
* \| \|	Slightly contracting code of evarconv.ml.	Hugo Herbelin	2016-02-28
\| \| *	Fixing bug #4596: [rewrite] broke in the past few weeks.	Pierre-Marie Pédrot	2016-02-28
* \| \|	Removing Tacmach.New qualification in Tacinterp.	Pierre-Marie Pédrot	2016-02-27
* \| \|	Removing some compatibility layers in Tacinterp.	Pierre-Marie Pédrot	2016-02-27
* \| \|	Qcabs : absolute value on normalized rational numbers Qc	Pierre Letouzey	2016-02-26
* \| \|	Qcanon : fix names of lemmas Qcle_alt & Qcge_alt (were Qle_alt & Qge_alt)	Pierre Letouzey	2016-02-26
* \| \|	Qcanon : implement some old suggestions by C. Auger	Pierre Letouzey	2016-02-26
\| \| *	Document Hint Mode, cleanup Hint doc.	Matthieu Sozeau	2016-02-24
* \| \|	Merge branch 'remove-quotations'	Pierre-Marie Pédrot	2016-02-24
\|\ \ \
\| * \| \|	Removing the METAIDENT token, as it is not used anymore.	Pierre-Marie Pédrot	2016-02-24
\| * \| \|	Removing the MetaIdArg entry of tactic expressions.	Pierre-Marie Pédrot	2016-02-24
\| * \| \|	Removing the Q_coqast module.	Pierre-Marie Pédrot	2016-02-24