| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-26 | Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if ↵ | Maxime Dénès | |
| printing only | |||
| 2017-05-26 | Merge PR#672: Add parsers-examples target to fiat-parsers ci | Maxime Dénès | |
| 2017-05-25 | Merge PR#416: Fix the way setoid_rewrite handles bindings. | Maxime Dénès | |
| 2017-05-23 | Add parsers-examples target to fiat-parsers ci | Jason Gross | |
| This tests a bit more of fiat-parsers, adding an extra ~3 minutes to the build. | |||
| 2017-05-23 | Fix bindings handling of setoid_rewrite. | Cyprien Mangin | |
| This fixes the discrepancy between "rewrite H with (1 := x)" and "setoid_rewrite H with (1 := x)". | |||
| 2017-05-20 | 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-19 | add test for Show with -emacs, bug 5535 | Paul Steckler | |
| 2017-05-17 | 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-16 | Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters). | Hugo Herbelin | |
| 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. | |||
| 2017-05-16 | 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-14 | Removing a line warned unused. | Hugo Herbelin | |
| 2017-05-14 | Removing a variable warned unused. | Hugo Herbelin | |
| 2017-05-10 | 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 | |
| "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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |