| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-10-10 | Add test file for #4416. | Maxime Dénès | |
| 2016-10-10 | Fix #4416: - Incorrect "Error: Incorrect number of goals" | Arnaud Spiwack | |
| In `Ftactic` the number of results could desynchronise with the number of goals when some goals were solved by side effect in a different branch of a `DISPATCH`. See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416). | |||
| 2016-10-09 | A tentative fix for #5102 (bullets parsing broken by calls to parse_entry). | Hugo Herbelin | |
| More precisely, commands that calls parse_entry put the lexer in an inconsistent state, breaking the lexing of bullet which relies on it. (Not to be pushed to v8.6 which has a better fix). | |||
| 2016-10-06 | evarconv.ml: Fix bug #4529, primproj unfolding | Matthieu Sozeau | |
| Evarconv was made precociously dependent on user-declared reduction behaviors. Only cbn should rely on that. | |||
| 2016-10-06 | w_merge: Add a comment about the (List.rev evars) | Matthieu Sozeau | |
| This change exposed bug #4763 | |||
| 2016-10-06 | unification.ml: fix for bug #4763, unif regression | Matthieu Sozeau | |
| Do not force all remaining conversions problems to be solved after the _first_ solution of an evar, but only at the end of assignment of terms to evars in w_merge. This was hell to track down, thanks for the help of Maxime. contribs pass and HoTT too. | |||
| 2016-10-03 | Fixing #4970 (confusion between special "{" and non special "{{" in notations). | Hugo Herbelin | |
| 2016-09-30 | Quick fix to another bug of "subst" introduced in 4e3d464 and spotted by Maxime. | Hugo Herbelin | |
| 2016-09-30 | Fix test-suite. | Maxime Dénès | |
| Restore subst output test file modified by mistake. | |||
| 2016-09-30 | Merge remote-tracking branch 'github/pr/294' into v8.5 | Maxime Dénès | |
| Was PR#294: Make error message more helpful. | |||
| 2016-09-30 | Merge branch '4762' into v8.5 | Maxime Dénès | |
| Was PR#293: Fix #4762 (eauto weaker than auto). | |||
| 2016-09-30 | Fix #4762. | Cyprien Mangin | |
| 2016-09-29 | Fix a bug in subst releaved by an OCaml warning. | Maxime Dénès | |
| 2016-09-28 | Make error message more helpful. | Théo Zimmermann | |
| CoqIDE does not have a "display" menu. It has a "view" menu with a list of display options. | |||
| 2016-09-27 | Fixing #4887 (confusion between using and with in documentation of firstorder). | Hugo Herbelin | |
| 2016-09-24 | Ensuring that the evar name is preserved by "rename" as it is already | Hugo Herbelin | |
| the case for clear and the conversion tactics. | |||
| 2016-09-22 | Fixing #5095 (non relevant too strict test in let-in abstraction). | Hugo Herbelin | |
| 2016-09-19 | Replace { command ; } with ( command ) | Erik Martin-Dorel | |
| as suggested by Hugo. Also, escape the spaces after the dots to obtain a better PdfLaTeX output. | |||
| 2016-09-19 | Fix typos in RefMan-uti.tex. | Erik Martin-Dorel | |
| - Ensure "coq_makefile --help" is properly typeset with HeVeA/PdfLaTeX - Replace 's with "s so they are typeset as true ASCII characters - Add missing ; before closing brace. | |||
| 2016-09-14 | Fixing test-suite after commit 43104a0b. | Pierre-Marie Pédrot | |
| 2016-09-12 | Fixing a recursive notation bug raised on coq-club on Sep 12, 2016. | Hugo Herbelin | |
| 2016-09-10 | Test for #5077. | Hugo Herbelin | |
| 2016-09-10 | Fixing #5077 (failure on typing a fixpoint with evars in its type). | Hugo Herbelin | |
| Typing.type_of was using conversion for types of fixpoints while it could have used unification. | |||
| 2016-09-09 | Restore native compiler optimizations after they were broken by 9e2ee58. | Maxime Dénès | |
| The greatest danger of OCaml's polymorphic equality is that PMP can replace it with pointer equality at any time, be warned :) The lack of optimization may account for an exponential blow-up in size of the generated code, as well as worse runtime performance. | |||
| 2016-09-05 | Test file for #5065 - Anomaly: Not a proof by induction | Maxime Dénès | |
| 2016-09-05 | Fix #5065: Anomaly: Not a proof by induction | Maxime Dénès | |
| Using abstract can create beta-redexes or let-ins in the head of the proof terms. The code projecting out mutual lemmas was not robust enough. | |||
| 2016-09-03 | Fixing what is probably a typo in Strict Proofs mode (#5062). | Hugo Herbelin | |
| 2016-09-01 | Fix test-suite after Frédéric's 6231f07b2. | Maxime Dénès | |
| 2016-09-01 | Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior). | Hugo Herbelin | |
| (It was reducing also in hypotheses.) | |||
| 2016-09-01 | Fixing name of internal refine ("simple refine"). | Hugo Herbelin | |
| 2016-08-31 | Fix bug #5043: [Admitted] lemmas pick up section variables. | Pierre-Marie Pédrot | |
| We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables. | |||
| 2016-08-30 | Fix #4871 - interrupting par:abstract kills coqtop | Maxime Dénès | |
| Fix done with Enrico. | |||
| 2016-08-30 | micromega cache files are now hidden files (cf #4156) | Frédéric Besson | |
| csdp.cache -> .csdp.cache lia.cache -> .lia.cache nlia.cache -> .nia.cache | |||
| 2016-08-30 | Setting an unknown option now always a warning. Fixes #4947. | Maxime Dénès | |
| Previously, setting an unknown option was an error or a warning, depending on the type of the option. We make it always a warning, for forward compatibility. This was already fixed in 8.6. | |||
| 2016-08-20 | Fixing an anomaly in printing a unification error message. | Hugo Herbelin | |
| 2016-08-19 | Remove extraneous dot in error message (bug #4832). | Guillaume Melquiond | |
| 2016-08-18 | Fix incorrect glob data for module symbols (bug #2336). | Guillaume Melquiond | |
| The logic was backward: if the path of a symbol was a prefix of the current path, then the current path (without sections) was used. But what we want is that, if the current path (without sections) is a prefix of the path of a symbol, then the former should be used. This fixes about 1,600 broken links in the documentation of the standard library. | |||
| 2016-08-17 | Fixing #5001 (metas not cleaned properly in clenv_refine_in). | Hugo Herbelin | |
| Fixing by copying what Matthieu did for Clenvtac.clenv_refine. | |||
| 2016-08-17 | Fixing CHANGES. | Hugo Herbelin | |
| Option Standard Proposition Elimination Scheme from 8.5 was not documented in the right section. | |||
| 2016-08-17 | infoH: output via msg_* to make the XML protocol happy | Enrico Tassi | |
| 2016-08-16 | Output a break before a list only if there was an empty line (bug #4606). | Guillaume Melquiond | |
| Moreover, this commit makes sure that an empty line after a list is always translated into a break. ("StartLevel 1" was excluded, for some reason.) It also avoids some code duplication. In particular, "stop_item ()" is defined as "reach_item_level 0", so there is no reason to handle "StartLevel 1" specially. | |||
| 2016-08-16 | Merge branch 'pr255' into v8.5 (bug #5015) | Guillaume Melquiond | |
| 2016-08-14 | Fix regression in Coqide's "forward one command" command | Xavier Leroy | |
| In Coqide 8.5pl2, "forward one command" (down arrow) always repositions the insertion point at the end of the phrase being executed, just after the final ".". In Coqide 8.4, the insertion point is not moved if it is after the end of the executed phrase. The insertion point is moved only if it falls behind the phrase being executed. I find the 8.5 behavior to be a regression over the lot more useful 8.4 behavior. This commit restores the 8.4 behavior of "forward one command". | |||
| 2016-08-11 | Do not assume the "TERM" environment variable is always set (bug #5007). | Guillaume Melquiond | |
| 2016-08-11 | Use the "md5" command on OpenBSD (bug #5008). | Guillaume Melquiond | |
| 2016-08-07 | Fix #5000: Document the native compiler soundness bug due to Unicode mangling. | Pierre-Marie Pédrot | |
| 2016-08-04 | Fix documentation typo (bug #4994). | Guillaume Melquiond | |
| 2016-07-29 | Fix bug #4673: regression in setoid_rewrite. | Matthieu Sozeau | |
| Modulo delta for types should be fully transparent. | |||
| 2016-07-29 | Update CHANGES about #3886 bugfix | Matthieu Sozeau | |
| 2016-07-29 | Fix bug #3886, generation of obligations of fixes | Matthieu Sozeau | |
| This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |