Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR#685: Fix a bug in checker | Maxime Dénès | 2017-05-29 |
|\ | |||
* \ | Merge PR#546: Fix for bug #4499 and other minor related bugs | Maxime Dénès | 2017-05-29 |
|\ \ | |||
| | * | Fix a bug in checker | Amin Timany | 2017-05-28 |
| |/ |/| | | | | | Universe constraints of the inductive types were not instantiated before being pushed on the environment. This commit fixes this bug. | ||
* | | Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show Match | Maxime Dénès | 2017-05-28 |
|\ \ | |||
* \ \ | Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if ↵ | Maxime Dénès | 2017-05-26 |
|\ \ \ | | | | | | | | | | | | | printing only | ||
* \ \ \ | Merge PR#672: Add parsers-examples target to fiat-parsers ci | Maxime Dénès | 2017-05-26 |
|\ \ \ \ | |||
| | | * | | Bug 5546, qualify datatype constructors when needed | Paul Steckler | 2017-05-25 |
| | | | | | |||
* | | | | | Merge PR#416: Fix the way setoid_rewrite handles bindings. | Maxime Dénès | 2017-05-25 |
|\ \ \ \ \ | |_|_|/ / |/| | | | | |||
| | * | | | Add parsers-examples target to fiat-parsers ci | Jason Gross | 2017-05-23 |
| |/ / / |/| | | | | | | | This tests a bit more of fiat-parsers, adding an extra ~3 minutes to the build. | ||
| * | | | Fix bindings handling of setoid_rewrite. | Cyprien Mangin | 2017-05-23 |
|/ / / | | | | | | | | | | | | | This fixes the discrepancy between "rewrite H with (1 := x)" and "setoid_rewrite H with (1 := x)". | ||
* | | | Merge PR#653: Bug #5535, test for Show with -emacs | Maxime Dénès | 2017-05-20 |
|\ \ \ | |||
* \ \ \ | Merge PR#641: Fix bug #5486, don't reverse ids in tuples | Maxime Dénès | 2017-05-20 |
|\ \ \ \ | |||
| | * | | | add test for Show with -emacs, bug 5535 | Paul Steckler | 2017-05-19 |
| |/ / / |/| | | | |||
| | * | | Fixing bug #5526,allow nonlinear variables in Notation patterns | Paul Steckler | 2017-05-17 |
| | | | | |||
| * | | | fix swapping of ids in tuples, bug 5486 | Paul Steckler | 2017-05-17 |
|/ / / | |||
* | | | Merge PR#635: Fixing #5522 (anomaly with free vars of pat) | Maxime Dénès | 2017-05-17 |
|\ \ \ | |||
| * | | | Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters). | Hugo Herbelin | 2017-05-16 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We seized this opportunity to factorize the code for interning `pat with more general pre-existing code. More precisely: There was already a function to compute the free variables of a pattern. Commit c6d9d4fb rewrote an approximation of it and #5222 hits cases non-treated by this function. We remove the partially-defined redundant code and use instead the existing code since intern_cases_pattern, already called, was already doing this computation. (In doing so, we discover a bug in merging names in the presence of nested "as" clauses, which we fix in previous commit. Additionally, intern_local_pattern was misleadingly overkill to simply mean a folding on Id.Set.add and we avoid the detour. | ||
| * | | | Fixing a bug with nested "as" clauses in "match". | Hugo Herbelin | 2017-05-16 |
| | | | | |||
* | | | | Merge PR#624: Switch bedrock to mit-plv base | Maxime Dénès | 2017-05-16 |
|\ \ \ \ | |/ / / |/| | | | |||
* | | | | Removing a line warned unused. | Hugo Herbelin | 2017-05-14 |
| | | | | |||
* | | | | Removing a variable warned unused. | Hugo Herbelin | 2017-05-14 |
| |/ / |/| | | |||
| * | | Switch bedrock to mit-plv base | Jason Gross | 2017-05-10 |
|/ / | |||
* | | Merge PR#604: FIx bug #5300: Anomaly: Uncaught exception Not_found" in ↵ | Maxime Dénès | 2017-05-10 |
|\ \ | | | | | | | | | | "Print Assumptions". | ||
* \ \ | 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-09 |
|\ \ \ \ | |||
| * | | | | Fix bug #3659: -time should understand multibyte encodings. | Pierre-Marie Pédrot | 2017-05-05 |
|/ / / / | | | | | | | | | | | | | | | | | 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. | ||
| | * / | 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-03 |
|/ / / | |||
* | | | Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions ↵ | Maxime Dénès | 2017-05-02 |
|\ \ \ | | | | | | | | | | | | | with evars). | ||
* \ \ \ | 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-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 |
|/ / |