coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \|	Merge branch 'yet-another-makefile-bigbang' into trunk	Pierre Letouzey	2016-06-01
\|\ \ \ \
\| * \| \| \|	Yet another Makefile reform : a unique phase without nasty make tricks	Pierre Letouzey	2016-06-01
\| * \| \| \|	Makefile: restore the use of coqdep_boot for creating .v.d files	Pierre Letouzey	2016-06-01
\| \| * \| \|	Fix potential race condition in vm_compute.	Guillaume Melquiond	2016-05-31
* \| \| \| \|	This patch splits pretty printing representation from IO operations.	Pierre-Marie Pédrot	2016-05-31
\|\ \ \ \ \ \| \|/ / / / \|/\| \| \| \|
\| \| * \| \|	Revert "Rename Lexer -> CLexer."	Pierre-Marie Pédrot	2016-05-31
* \| \| \| \|	Making the grammar/ folder independent from the other ones.	Pierre-Marie Pédrot	2016-05-31
\| * \| \| \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
\|/ / / /
* \| \| \|	Checker: avoid using obsolete names from Names	Pierre Letouzey	2016-05-31
* \| \| \|	Checker: no more -I kernel via a few symlinks (for Names and Esubst)	Pierre Letouzey	2016-05-31
\| * \| \|	Extraction : add a location in the error message about polyprop	Pierre Letouzey	2016-05-30
* \| \| \|	Extraction : add a location in the error message about polyprop	Pierre Letouzey	2016-05-30
\| * \| \|	Fix bug #4746: Anomaly: Evar ?X10 was not declared.	Pierre-Marie Pédrot	2016-05-29
\| * \| \|	STM: fix argument filtering for slaves	Enrico Tassi	2016-05-27
\| * \| \|	Pfedit.get_current_context refinement (fix #4523)	Matthieu Sozeau	2016-05-26
\| * \| \|	rewrite/Univs: Fix bug # 4498.	Matthieu Sozeau	2016-05-26
* \| \| \|	Update required OCaml version in configure.	Maxime Dénès	2016-05-26
\| * \| \|	Extraction/Projections: Fix bug #4710	Matthieu Sozeau	2016-05-23
\| * \| \|	Hints/Univs: fix bug #4628 anomalies	Matthieu Sozeau	2016-05-23
* \| \| \|	typos	Enrico Tassi	2016-05-23
\| * \| \|	Disable memoization rather than failing when files cannot be opened.	Guillaume Melquiond	2016-05-20
* \| \| \|	Extraction: code cleanup in Common	Pierre Letouzey	2016-05-20
* \| \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-20
\|\\| \| \|
\| * \| \|	native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)	Pierre Letouzey	2016-05-19
\| * \| \|	Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)	Pierre Letouzey	2016-05-19
* \| \| \|	native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)	Pierre Letouzey	2016-05-19
* \| \| \|	Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)	Pierre Letouzey	2016-05-19
\| * \| \|	adding "user-contrib" directory to ".gitignore"	Matej Kosik	2016-05-19
\| * \| \|	Unicode.ascii_of_ident is now truly injective	Pierre Letouzey	2016-05-19
* \| \| \|	Unicode.ascii_of_ident is now truly injective	Pierre Letouzey	2016-05-19
* \| \| \|	Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new Init/...	Pierre Letouzey	2016-05-19
* \| \| \|	Putting all the tactics exported by the Tactics module in the new monad API.	Pierre-Marie Pédrot	2016-05-17
\|\ \ \ \
\| * \| \| \|	Removing some compatibility layers in Tactics.	Pierre-Marie Pédrot	2016-05-17
\| * \| \| \|	Removing the old refine tactic from the Tactics module.	Pierre-Marie Pédrot	2016-05-17
\| * \| \| \|	Put the "move" tactic in the monad.	Pierre-Marie Pédrot	2016-05-17
\| * \| \| \|	Put the "change" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \| \| \|	Put the "specialize_eq" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \| \| \|	Put the "generalize dependent" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \| \| \|	Put the "generalize" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \| \| \|	Put the "cofix" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \| \| \|	Put the "*_cast_no_check" tactics in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \| \| \|	Put the "exact" family of tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \| \| \|	Put the "fix" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \| \| \|	Put the "exact_constr" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
\| * \| \| \|	Put the "clear" tactic into the monad.	Pierre-Marie Pédrot	2016-05-16
\|/ / / /
\| * \| \|	Fix bug #4737: cycle tactic doesn't like zero goals.	Pierre-Marie Pédrot	2016-05-16
* \| \| \|	Generate more user-readable tactic notation kernel names.	Pierre-Marie Pédrot	2016-05-16
* \| \| \|	Merge pull request #170 from relrod/patch-1	Pierre-Marie Pédrot	2016-05-16
\|\ \ \ \
\| * \| \| \|	Fix a really small doc typo	Ricky Elrod	2016-05-15
\|/ / / /
\| * \| \|	Removing unexcepted activation of option "Regular Subst Tactic", since	Hugo Herbelin	2016-05-14