coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
* \| \| \| \| \|	Merge PR#599: Repairing `Set Rewriting Schemes`	Maxime Dénès	2017-05-02
\|\ \ \ \ \ \
* \| \| \| \| \| \|	Avoiding registering files from _build_ci when not calling Makefile.ci.	Hugo Herbelin	2017-05-02
\| \| \| \| \| \| \|
\| \| \| \| * \| \|	Add bmsherman/topology to the ci	Jason Gross	2017-05-01
\| \|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This development of @bmsherman tests universe polymorphism and setoid rewriting in type, and should build with v8.6 and trunk.
\| * \| \| \| \|	Fixing Set Rewriting Schemes bugs introduced in v8.5.	Hugo Herbelin	2017-05-01
\|/ / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Fixing a typo introduced in 31dbba5f. - Adapting to computation of universe constraints in pretyping. - Adding a regression test.
\| * \| \| \|	remove unneeded -emacs flag to coq-prog-args	Paul Steckler	2017-05-01
\| \| \| \| \|
\| \| * \| \|	Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).	Hugo Herbelin	2017-05-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The fix follows an invariant enforced in proofview.ml on the kind of evars that are goals or that occur in goals. One day, evar kinds will need a little cleaning... PS: This is a second attempt, completing db28e82 which was missing the case PEvar in constr_matching.ml. Indeed the attached fix to #5487 alone made #2602 failing, revealing that the real cause for #2602 was actually not fixed and that if the test for #2602 was working it was because of #5487 hiding the real problem in #2602.
\| \| * \| \|	Really fixing #2602 which was wrongly working because of #5487 hiding the cause.	Hugo Herbelin	2017-05-01
\| \|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The cause was a missing evar/evar clause in ltac pattern-matching function (constr_matching.ml).
* \| \| \|	Answer to db28e827d: I did test the commit on test-suite but for some	Hugo Herbelin	2017-05-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	reason I overlooked the result, maybe a missing make clean. As for testing on the travis test architecture, I could have done it. This is a question of compromise. I was so certain that it would work that I did not test. And anyway, the travis test is not absolute either. In any case, I'm very sorry about the confusion it introduced. ~~~~ BY THE WAY, NO NEED TO SHOUT ~~~~ ~~~~ IT IS A BIG MISCONCEPTION ABOUT HUMAN BEINGS ~~~~ ~~~~ TO BELIEVE THAT THEY DO MISTAKES INTENTIONALLY ~~~~ Thank you!
* \| \| \|	Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."	Maxime Dénès	2017-04-28
\|/ / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	One day I'll get bored of spending my nights fixing commits that were pushed without being tested, and I'll ask for removal of push rights. But for now let's pretend I haven't insisted enough: ~~~~ PLEASE TEST YOUR COMMITS BEFORE PUSHING ~~~~ Thank you!
* \| \|	Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).	Hugo Herbelin	2017-04-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The fix follows an invariant enforced in proofview.ml on the kind of evars that are goals or that occur in goals. One day, evar kinds will need a little cleaning...
* \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Due to code reworking, a fastpath got anihilated because the slow path was computed altogether. We now only compute the slow check whenever the quick one fails.
* \| \|	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
\| \|_\|/ \|/\| \| \| \| \| \| \| \|	Add a test-suite file to be sure we won't regress silently.
* \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was assuming dependencies occurring in configurations of the form x:A, y:B x, z:C x y \|- match x, y, z with ... end". But still work to do for better management of dependencies in general...
\| \| \| *	Better support for printing constructors with let-ins.	Hugo Herbelin	2017-04-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This allows e.g. to use the record notations even when there are defined fields. A priori fixed also missing parameters when interpreting primitive tokens.
\| \| \| *	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
\| \|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This fixes a few clear bugs, but the STM code handling Time, Fail and Redirect before par: still needs to be rewritten. It does not implement the same semantics as the vernac interpreter for Fail Fail [c] and ignores Redirect. This commit was already reviewed with Enrico and tested on Travis.
* \| \|	Merge branch 'origin/v8.5' into v8.6.	Hugo Herbelin	2017-04-06
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	Was needed to be done for a while.
* \| \| \|	Fixing #5454 (an assert false with 'pat).	Hugo Herbelin	2017-04-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Note: Apparently not easy to make a test file as the error is raised in "G_vernac.fresh_var" at parsing time (not captured by Fail).
\| \| \| *	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
\|/ / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was introduced by 4f041384cb27f0d2. Unsoundness seems miraculously avoided by a safeguard I put in nativecode.ml. But other kernel changes in this commit should probably be reviewed carefully.
* \| \|	Merge PR#533: Instances should obey universe binders even when defined by ↵	Maxime Dénès	2017-04-03
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	tactics.
\| * \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Bug #4957 was "unify cannot directly unify universes with evars, but can do so indirectly".
* \| \|	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
\| \|/ / / \|/\| \| \|