| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-06-19 | Change CoqIDE-specific to neutral wording | Paul Steckler | |
| 2017-06-16 | Merge PR#730: Protecting from warnings while compiling 8.6 | Maxime Dénès | |
| 2017-06-16 | Merge PR#767: Document named evars (including Show ident) | Maxime Dénès | |
| 2017-06-15 | Merge PR#741: Fix documentation of Typeclasses eauto := | Maxime Dénès | |
| 2017-06-15 | Merge PR#713: Bump year in headers. | Maxime Dénès | |
| 2017-06-15 | 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-13 | Document instantiate (ident := term) and make it the preferred variant. | Théo Zimmermann | |
| 2017-06-13 | Document Show ident. | Théo Zimmermann | |
| 2017-06-13 | Document evar naming syntax. | Théo Zimmermann | |
| 2017-06-09 | Fix Bug #5568, no dup notation warnings on repeated module imports | Paul Steckler | |
| 2017-06-08 | Adding a test case as requested in bug 5205. | Théo Zimmermann | |
| 2017-06-07 | Fix documentation of Typeclasses eauto := | Théo Zimmermann | |
| 2017-06-05 | Univs: fix bug #5365, generation of u+k <= v constraints | Matthieu Sozeau | |
| Use an explicit label ~algebraic for make_flexible_variable as well. | |||
| 2017-06-04 | Ensure that warnings new from ocaml > 4.01 remains silent. | Hugo Herbelin | |
| Indeed, 8.6 is announced to be compilable with 4.01.0 and it is convenient not seeing warnings about which nothing can be done. Remove deprecation warnings new from ocaml 4.03, as well as warning 52. This is a partial cherry-pick of a77734ad6. | |||
| 2017-06-04 | configure: avoid deprecated warnings | Pierre Letouzey | |
| 2017-06-02 | Merge PR#705: Fix bug #5019 (looping zify on dependent types) | Maxime Dénès | |
| 2017-06-01 | Merge PR#631: Fix bug #5255 | Maxime Dénès | |
| 2017-06-01 | Bump year in headers. | Maxime Dénès | |
| 2017-06-01 | Fix bug #5019 (looping zify on dependent types) | Jason Gross | |
| 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. | |||
| 2017-06-01 | 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-05-31 | Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake ↵ | Maxime Dénès | |
| (EDIT: for mutual fixpoints) | |||
| 2017-05-31 | Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with ↵ | Maxime Dénès | |
| section variables. | |||
| 2017-05-30 | 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-29 | Omega: use "simpl" only on coefficents, not on atoms (fix #4132) | Pierre Letouzey | |
| 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). | |||
| 2017-05-29 | 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-28 | Fix a bug in checker | Amin Timany | |
| Universe constraints of the inductive types were not instantiated before being pushed on the environment. This commit fixes this bug. | |||
| 2017-05-28 | Fixing a subtle bug in tclWITHHOLES. | Hugo Herbelin | |
| This fixes Théo's bug on eset. | |||
| 2017-05-28 | Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show Match | Maxime Dénès | |
| 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 | 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-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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |