aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-10-12Merge remote-tracking branch 'github/pr/286' into v8.5Maxime Dénès
Was PR#286: Fix the definition of if_then_else for tactics with multiple success.
2016-10-12Merge remote-tracking branch 'git/bug5123' into v8.5Matthieu Sozeau
2016-10-11Fix test-suite file 5123 to fail in case of regressionMatthieu Sozeau
2016-10-11Merge remote-tracking branch 'github/bug4863' into v8.5Matthieu Sozeau
2016-10-11Fix bug #5123: mark all shelved evars unresolvableMatthieu Sozeau
Previously, some splipped through and were caught by unrelated calls to typeclass resolution.
2016-10-11Fix for bug #4863, update the Proofview's env withMatthieu Sozeau
side_effects. Partial solution to the handling of side effects in proofview.
2016-10-10Add test file for #4416.Maxime Dénès
2016-10-10Fix #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-09A 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-06evarconv.ml: Fix bug #4529, primproj unfoldingMatthieu Sozeau
Evarconv was made precociously dependent on user-declared reduction behaviors. Only cbn should rely on that.
2016-10-06w_merge: Add a comment about the (List.rev evars)Matthieu Sozeau
This change exposed bug #4763
2016-10-06unification.ml: fix for bug #4763, unif regressionMatthieu 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-03Fixing #4970 (confusion between special "{" and non special "{{" in notations).Hugo Herbelin
2016-10-03Remove if_then_else. Use tryif instead.Théo Zimmermann
if_then_else definition does not account for multi success tactics. tryif_then_else is a primitive tactical with the expected behavior.
2016-09-30Quick fix to another bug of "subst" introduced in 4e3d464 and spotted by Maxime.Hugo Herbelin
2016-09-30Fix test-suite.Maxime Dénès
Restore subst output test file modified by mistake.
2016-09-30Merge remote-tracking branch 'github/pr/294' into v8.5Maxime Dénès
Was PR#294: Make error message more helpful.
2016-09-30Merge branch '4762' into v8.5Maxime Dénès
Was PR#293: Fix #4762 (eauto weaker than auto).
2016-09-30Fix #4762.Cyprien Mangin
2016-09-29Fix a bug in subst releaved by an OCaml warning.Maxime Dénès
2016-09-28Make 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-27Fixing #4887 (confusion between using and with in documentation of firstorder).Hugo Herbelin
2016-09-24Ensuring that the evar name is preserved by "rename" as it is alreadyHugo Herbelin
the case for clear and the conversion tactics.
2016-09-22Fixing #5095 (non relevant too strict test in let-in abstraction).Hugo Herbelin
2016-09-19Replace { 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-19Fix 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-14Fixing test-suite after commit 43104a0b.Pierre-Marie Pédrot
2016-09-12Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.Hugo Herbelin
2016-09-10Test for #5077.Hugo Herbelin
2016-09-10Fixing #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-09Restore 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-05Test file for #5065 - Anomaly: Not a proof by inductionMaxime Dénès
2016-09-05Fix #5065: Anomaly: Not a proof by inductionMaxime 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-03Fixing what is probably a typo in Strict Proofs mode (#5062).Hugo Herbelin
2016-09-01Fix test-suite after Frédéric's 6231f07b2.Maxime Dénès
2016-09-01Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior).Hugo Herbelin
(It was reducing also in hypotheses.)
2016-09-01Fixing name of internal refine ("simple refine").Hugo Herbelin
2016-08-31Fix 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-30Fix #4871 - interrupting par:abstract kills coqtopMaxime Dénès
Fix done with Enrico.
2016-08-30micromega 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-30Setting 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-20Fixing an anomaly in printing a unification error message.Hugo Herbelin
2016-08-19Remove extraneous dot in error message (bug #4832).Guillaume Melquiond
2016-08-18Fix 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-17Fixing #5001 (metas not cleaned properly in clenv_refine_in).Hugo Herbelin
Fixing by copying what Matthieu did for Clenvtac.clenv_refine.
2016-08-17Fixing CHANGES.Hugo Herbelin
Option Standard Proposition Elimination Scheme from 8.5 was not documented in the right section.
2016-08-17infoH: output via msg_* to make the XML protocol happyEnrico Tassi
2016-08-16Output 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-16Merge branch 'pr255' into v8.5 (bug #5015)Guillaume Melquiond
2016-08-14Fix regression in Coqide's "forward one command" commandXavier 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".
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 17:33:40 +0000