| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |||
| 2016-07-29 | Fix #4769, univ poly and elim schemes in sections | Matthieu Sozeau | |
| 2016-07-26 | Update CHANGES about critical bugfix and others | Matthieu Sozeau | |
| 2016-07-26 | Merge branch 'bug4754' into v8.5 | Matthieu Sozeau | |
| 2016-07-26 | Fix bug #4754, allow conversion problems to remain | Matthieu Sozeau | |
| when checking that the rewrite relation is homogeneous in setoid_rewrite. | |||
| 2016-07-26 | Merge branch 'bug4876' into v8.5 | Matthieu Sozeau | |
| 2016-07-25 | Fix bug #4876: critical bug in guard condition checker. | Matthieu Sozeau | |
| 2016-07-20 | Update CHANGES | Matthieu Sozeau | |
| 2016-07-20 | Fix bug #4780: universe leak in letin_tac | Matthieu Sozeau | |
| 2016-07-19 | Fix Errors.out missing a dot... | Matthieu Sozeau | |
| 2016-07-13 | Fixing printing of evar name in an error message of instantiate. | Hugo Herbelin | |
| 2016-07-13 | Typo. | Hugo Herbelin | |
| 2016-07-08 | Add a few fixes in CHANGES that were forgotten. | Maxime Dénès | |
| We should really automate the generation of the log of fixes for CHANGES. | |||
| 2016-07-08 | Fix test file for #4858. | Maxime Dénès | |
| 2016-07-08 | Update csdp.cache. | Maxime Dénès | |
| 2016-07-08 | Test file for #4858. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |