| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-14 | Removing a line warned unused. | Hugo Herbelin | |
| 2017-05-14 | Removing a variable warned unused. | Hugo Herbelin | |
| 2017-05-10 | Merge PR#604: FIx bug #5300: Anomaly: Uncaught exception Not_found" in ↵ | Maxime Dénès | |
| "Print Assumptions". | |||
| 2017-05-09 | Merge PR#591: Add bmsherman/topology to the ci | Maxime Dénès | |
| 2017-05-09 | Put .travis.yml in alphabetical order | Jason Gross | |
| 2017-05-09 | Merge PR#609: Fix bug #3659: -time should understand multibyte encodings. | Maxime Dénès | |
| 2017-05-05 | Fix bug #3659: -time should understand multibyte encodings. | Pierre-Marie Pédrot | |
| We assume Coq always outputs UTF-8 (is it really the case?) and cut strings after 30 UTF-8 characters instead of using the standard String function. | |||
| 2017-05-03 | FIx bug #5300: uncaught exception in "Print Assumptions". | Cyprien Mangin | |
| 2017-05-03 | Merge PR#603: Fix outdated description in RefMan. | Maxime Dénès | |
| 2017-05-03 | Fix outdated description in RefMan. | Théo Zimmermann | |
| 2017-05-02 | Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions ↵ | Maxime Dénès | |
| with evars). | |||
| 2017-05-02 | Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite files | Maxime Dénès | |
| 2017-05-02 | 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-01 | Add bmsherman/topology to the ci | Jason Gross | |
| This development of @bmsherman tests universe polymorphism and setoid rewriting in type, and should build with v8.6 and trunk. | |||
| 2017-05-01 | Fixing Set Rewriting Schemes bugs introduced in v8.5. | Hugo Herbelin | |
| - Fixing a typo introduced in 31dbba5f. - Adapting to computation of universe constraints in pretyping. - Adding a regression test. | |||
| 2017-05-01 | 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 | |
| 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. | |||
| 2017-05-01 | Really fixing #2602 which was wrongly working because of #5487 hiding the cause. | Hugo Herbelin | |
| The cause was a missing evar/evar clause in ltac pattern-matching function (constr_matching.ml). | |||
| 2017-05-01 | Answer to db28e827d: I did test the commit on test-suite but for some | Hugo Herbelin | |
| 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! | |||
| 2017-04-28 | Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)." | Maxime Dénès | |
| 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! | |||
| 2017-04-28 | Fixing #5487 (v8.5 regression on ltac-matching expressions with evars). | Hugo Herbelin | |
| 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... | |||
| 2017-04-27 | 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-25 | Fix an optimization failure in tclPROGRESS. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-04-25 | Merge PR#567: Fix bug #5377: @? patterns broken. | Maxime Dénès | |
| 2017-04-24 | Merge PR#577: Add bedrock targets src and facade to Travis CI | Maxime Dénès | |
| 2017-04-20 | Add bedrock targets src and facade | Jason Gross | |
| 2017-04-20 | Fix bug #5377: @? patterns broken. | Pierre-Marie Pédrot | |
| 2017-04-19 | Merge PR#538: Correction of bug #4306 | Maxime Dénès | |
| 2017-04-14 | 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-13 | update XML protocol doc to 8.6 | Paul Steckler | |
| 2017-04-13 | add XML protocol doc for 8.5 | Paul Steckler | |
| 2017-04-12 | Merge PR#510: Correctly identify [Time Defined.] as a defined | Maxime Dénès | |
| 2017-04-08 | Fixing #5460 (limitation in computing deps in pattern-matching compilation). | Hugo Herbelin | |
| 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... | |||
| 2017-04-06 | Fix a few programming pearls related to Time, Fail and Redirect. | Maxime Dénès | |
| 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. | |||
| 2017-04-06 | Merge branch 'origin/v8.5' into v8.6. | Hugo Herbelin | |
| Was needed to be done for a while. | |||
| 2017-04-05 | Fixing #5454 (an assert false with 'pat). | Hugo Herbelin | |
| 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). | |||
| 2017-04-04 | 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |