Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraints | Maxime Dénès | 2017-06-15 |
|\ | |||
* \ | Merge PR#752: Adding a test case as requested in bug 5205. | Maxime Dénès | 2017-06-15 |
|\ \ | |||
* \ \ | Merge PR#747: Fix Bug #5568, no dup notation warnings on repeated module imports | Maxime Dénès | 2017-06-15 |
|\ \ \ | |||
| * | | | Fix Bug #5568, no dup notation warnings on repeated module imports | Paul Steckler | 2017-06-09 |
| | | | | |||
| | * | | Adding a test case as requested in bug 5205. | Théo Zimmermann | 2017-06-08 |
| |/ / |/| | | |||
| | * | Univs: fix bug #5365, generation of u+k <= v constraints | Matthieu Sozeau | 2017-06-05 |
| | | | | | | | | | | | | Use an explicit label ~algebraic for make_flexible_variable as well. | ||
* | | | Merge PR#705: Fix bug #5019 (looping zify on dependent types) | Maxime Dénès | 2017-06-02 |
|\ \ \ | |/ / |/| | | |||
* | | | Merge PR#631: Fix bug #5255 | Maxime Dénès | 2017-06-01 |
|\ \ \ | |||
| | * | | Fix bug #5019 (looping zify on dependent types) | Jason Gross | 2017-06-01 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes [bug #5019](https://coq.inria.fr/bugs/show_bug.cgi?id=5019), "[zify] loops on dependent types"; before, we would see a `Z.of_nat (S ?k)` which could not be turned into `Z.succ (Z.of_nat k)`, add a hypothesis of the shape `0 <= Z.of_nat (S k)`, turn that into a hypothesis of the shape `0 <= Z.succ (Z.of_nat k)`, and loop forever on this. This may not be the "right" fix (there may be cases where `zify` should succeed where it still fails with this change), but this is a pure bugfix in the sense that the only places where it changes the behavior of `zify` are the places where, previously, `zify` looped forever. | ||
| | * | | Add opened bug 5019 | Jason Gross | 2017-06-01 |
| | | | | |||
* | | | | Merge PR#710: Add test-suite checks for coqchk with constraints | Maxime Dénès | 2017-06-01 |
|\ \ \ \ | |_|/ / |/| | | | |||
* | | | | Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake ↵ | Maxime Dénès | 2017-05-31 |
|\ \ \ \ | | | | | | | | | | | | | | | | (EDIT: for mutual fixpoints) | ||
* \ \ \ \ | Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with ↵ | Maxime Dénès | 2017-05-31 |
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | section variables. | ||
| | | * | | | Add test-suite checks for coqchk with constraints | Jason Gross | 2017-05-30 |
| |_|/ / / |/| | | | | |||
* | | | | | Merge PR#693: A subtle bug in tclWITHHOLES. | Maxime Dénès | 2017-05-30 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR#695: Omega: fix bug #4132 | Maxime Dénès | 2017-05-30 |
|\ \ \ \ \ \ | |||
| | | * | | | | Fix bug 5550: "typeclasses eauto with" does not work with section variables. | Théo Zimmermann | 2017-05-30 |
| |_|/ / / / |/| | | | | | |||
| * | | | | | Omega: use "simpl" only on coefficents, not on atoms (fix #4132) | Pierre Letouzey | 2017-05-29 |
|/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Two issues in one: - some focused_simpl were called on the wrong locations - some focused_simpl were done on whole equations In the two cases, this could be bad if "simpl" goes too far with respect to what omega expects: later calls to "occurrence" might fail. This may happen for instance if an atom isn't a variable, but a let-in (b:=5:Z in the example). | ||
* | | | | | 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. | ||
| | * | | | | Fixing a subtle bug in tclWITHHOLES. | Hugo Herbelin | 2017-05-28 |
| |/ / / / |/| | | | | | | | | | | | | | | This fixes Théo's bug on eset. | ||
* | | | | | 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 |
|\ \ \ \ \ \ \ | |/ / / / / / |/| | | | | | | |||
| | | | | * | | Fix #5255: [Context (x : T := y)] should mean [Let x := y]. | Pierre-Marie Pédrot | 2017-05-15 |
| | | |_|/ / | | |/| | | | |||
* | | | | | | 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 |
|/ / / / / |