coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \|	Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).	Hugo Herbelin	2017-04-28
* \| \|	Merge PR#587: Fix description of command-line arguments for Add (Rec) LoadPath	Maxime Dénès	2017-04-27
\|\ \ \
\| * \| \|	fix order of command-line arguments mentioned in Add LoadPath	Paul Steckler	2017-04-27
\|/ / /
* \| \|	Test for bug #5193: Uncaught exception Class_tactics.Search.ReachedLimitEx.	Pierre-Marie Pédrot	2017-04-27
* \| \|	Fix an optimization failure in tclPROGRESS.	Pierre-Marie Pédrot	2017-04-25
* \| \|	Merge PR#567: Fix bug #5377: @? patterns broken.	Maxime Dénès	2017-04-25
\|\ \ \
* \ \ \	Merge PR#577: Add bedrock targets src and facade to Travis CI	Maxime Dénès	2017-04-24
\|\ \ \ \
\| * \| \| \|	Add bedrock targets src and facade	Jason Gross	2017-04-20
\|/ / / /
\| * / /	Fix bug #5377: @? patterns broken.	Pierre-Marie Pédrot	2017-04-20
\|/ / /
* \| \|	Merge PR#538: Correction of bug #4306	Maxime Dénès	2017-04-19
\|\ \ \
* \| \| \|	Fixing bug #5470 (anomaly on notations with misused "binder" type).	Hugo Herbelin	2017-04-14
* \| \| \|	Fixing bug #5469 (notation format not recognizing curly braces).	Hugo Herbelin	2017-04-14
* \| \| \|	Fix EOL characters in xml protocol documentation.	Maxime Dénès	2017-04-14
* \| \| \|	Merge PR#556: Fix anomaly when doing [all:Check _.] during a proof.	Maxime Dénès	2017-04-14
\|\ \ \ \
\| * \| \| \|	Fix anomaly when doing [all:Check _.] during a proof.	Gaetan Gilbert	2017-04-14
* \| \| \| \|	Merge PR#563: add XML protocol doc for 8.6	Maxime Dénès	2017-04-14
\|\ \ \ \ \
* \| \| \| \| \|	[travis] Use the lite target for fiat-crypto.	Maxime Dénès	2017-04-14
\| \|/ / / / \|/\| \| \| \|
\| * \| \| \|	update XML protocol doc to 8.6	Paul Steckler	2017-04-13
\| * \| \| \|	add XML protocol doc for 8.5	Paul Steckler	2017-04-13
\|/ / / /
\| \| \| *	Reinstate fixpoint refolding in [cbn], deactivated by mistake.	Matthieu Sozeau	2017-04-13
\| \|_\|/ \|/\| \|
* \| \|	Merge PR#510: Correctly identify [Time Defined.] as a defined	Maxime Dénès	2017-04-12
\|\ \ \
* \| \| \|	Fixing #5460 (limitation in computing deps in pattern-matching compilation).	Hugo Herbelin	2017-04-08
\| \| \| *	Better support for printing constructors with let-ins.	Hugo Herbelin	2017-04-07
\| \| \| *	Fixing #4499 (not using unnamed record field in {\| \|} notation).	Hugo Herbelin	2017-04-07
* \| \| \|	Fix a few programming pearls related to Time, Fail and Redirect.	Maxime Dénès	2017-04-06
\| \|_\|/ \|/\| \|
* \| \|	Merge branch 'origin/v8.5' into v8.6.	Hugo Herbelin	2017-04-06
\|\ \ \
* \| \| \|	Fixing #5454 (an assert false with 'pat).	Hugo Herbelin	2017-04-05
\| \| \| *	closing bug file for #4306	Julien Forest	2017-04-04
\| \| \| *	end of correction of bug 4306	Julien Forest	2017-04-04
\| \| \| *	Bad correction in previous commit	Julien Forest	2017-04-04
\| \| \| *	Solving first problem in bug #4306. TO DO : solve the let in problem	Julien Forest	2017-04-04
\| \| \| *	bug file for 4306	Julien Forest	2017-04-04
* \| \| \|	Merge PR#535: Fix #5435: [Eval native_compute in] raises anomaly.	Maxime Dénès	2017-04-04
\|\ \ \ \ \| \|_\|_\|/ \|/\| \| \|
\| * \| \|	Test file for #5435: [Eval native_compute in] raises anomaly.	Maxime Dénès	2017-04-04
\| * \| \|	Fix bug #5435: [Eval native_compute in] raises anomaly.	Maxime Dénès	2017-04-04
\|/ / /
* \| \|	Merge PR#533: Instances should obey universe binders even when defined by tac...	Maxime Dénès	2017-04-03
\|\ \ \
\| * \| \|	Instances should obey universe binders even when defined by tactics.	Gaetan Gilbert	2017-04-03
\|/ / /
* \| \|	Add test file for #4957.	Maxime Dénès	2017-04-03
* \| \|	Merge PR#463: Run non-tactic comands without resilient_command	Maxime Dénès	2017-03-30
\|\ \ \
* \ \ \	Merge PR#514: [travis] Backport from trunk: VST	Maxime Dénès	2017-03-29
\|\ \ \ \
\| \| * \| \|	Run non-tactic comands without resilient_command	Tej Chajed	2017-03-29
\| \|/ / / \|/\| \| \|
\| * \| \|	[travis] Backport from trunk: VST	Emilio Jesus Gallego Arias	2017-03-24
\|/ / /
* \| \|	Merge PR#476: [future] Be eager when "chaining" already resolved future values.	Maxime Dénès	2017-03-24
\|\ \ \
* \ \ \	Merge PR#475: Opaque side effects	Maxime Dénès	2017-03-24
\|\ \ \ \
\| \| \| \| *	Correctly identify [Time Defined.] as a defined	Tej Chajed	2017-03-23
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	Merge PR#507: Intern names bound in match patterns	Maxime Dénès	2017-03-23
\|\ \ \ \
\| \| * \| \|	Documenting the API of side-effects.	Pierre-Marie Pédrot	2017-03-23
\| \| * \| \|	Using a dedicated datastructure for side effect ordering.	Pierre-Marie Pédrot	2017-03-23
\| \| * \| \|	Making the side_effects type opaque.	Pierre-Marie Pédrot	2017-03-23
\| \|/ / / \|/\| \| \|
\| * \| \|	Intern names bound in match patterns	Tej Chajed	2017-03-23