aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2015-02-14dependent destruction: Fix (part of) bug #3961, by fixing dependent *Matthieu Sozeau
generalizing * which was broken since 8.4.
2015-02-14coqc accepts -top option. Fixes bug #4043.Pierre-Marie Pédrot
2015-02-14Univs: fix bug #3755. We were missing refreshements of universes inMatthieu Sozeau
unifications ?X ~= ?Y foo not catched by solve_evar_evar.
2015-02-14Univs: When computing the level of an inductive including indices, letsMatthieu Sozeau
do not contribute. Fixes bug #3808.
2015-02-13Document the issue with trivial inductive types. (Workaround for bug #3984)Guillaume Melquiond
2015-02-13Fixup version & copyright for MacOS bundlePierre Boutillier
2015-02-13Hardcode how coqide have to look for coqtop in MacOS bundlePierre Boutillier
Sorry, that is ugly. Please revert if you see a better way to do it.
2015-02-13Better error message for nested module application.Maxime Dénès
Fixes #3809.
2015-02-13Fix test-suite file to finishMatthieu Sozeau
2015-02-13Selection of the current word in CoqIDE looks at all buffers.Pierre-Marie Pédrot
2015-02-13Trying to fix bug #3930.Pierre-Marie Pédrot
Instead of setting the last modified part of the text to be the insert point, we register all modifications to the buffer between to user actions and take the last modified point to be the least offset of all those modifications.
2015-02-12Fixed test-suite file, that should always work.Matthieu Sozeau
2015-02-12Add test-suite files for closed bugs.Matthieu Sozeau
2015-02-12Tentative fix for CoqIDE randomly dropping deletions.Pierre-Marie Pédrot
We make the deletion callback not to regenerate a task id, as the insertion callback does. I can't find a particular reason for this dissymetry, and it was indeed causing trouble.
2015-02-12COMPATIBILITY: add note about the change of behavior of Instance foo :=Matthieu Sozeau
{| |}. Add test-suite files for closed bugs.
2015-02-12Univs: fix bug #4031: wrong folding of sigma in change.Matthieu Sozeau
2015-02-12Univs: fix bug #3978: carry around the universe context used toMatthieu Sozeau
typecheck with definitions and thread it accordingly when typechecking module expressions.
2015-02-12Fix bug #2775: Correct handling of universes in leminv.Matthieu Sozeau
2015-02-12Fix typos about .vio files (thanks Arthur for spotting them)Enrico Tassi
2015-02-12Fixing bug #3261.Pierre-Marie Pédrot
2015-02-12Focussing on message view in CoqIDE when a message is pushed.Pierre-Marie Pédrot
Also fixes bug #4030.
2015-02-12Revert "Using same code for browsing physical directories in coqtop and coqdep."Hugo Herbelin
(Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
2015-02-12Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Hugo Herbelin
This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767.
2015-02-12Capital letter in plugins.Hugo Herbelin
2015-02-12Using same code for browsing physical directories in coqtop and coqdep.Hugo Herbelin
In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error).
2015-02-12Fixing #3982 (conflict with max notation for universes).Hugo Herbelin
2015-02-12Fixing #3997 (occur-check in the presence of primitive projections, patchHugo Herbelin
from Matthieu).
2015-02-12Fixing bug #4023.Pierre-Marie Pédrot
2015-02-12Fixing compilation for 3.12.Pierre-Marie Pédrot
2015-02-12Tentative fix for bug #4027.Pierre-Marie Pédrot
2015-02-12Make clearer that "Remove Printing Let" does not influence destructuring let.Guillaume Melquiond
2015-02-11Adding test for bug #3786.Pierre-Marie Pédrot
2015-02-11Missing space in error messageMatěj Grabovský
2015-02-11Win: use .exe extension for the ocaml compiler (Close 3572)Enrico Tassi
2015-02-11STM: is Flags.async_proofs_full then always delegateEnrico Tassi
Probably a regression introduced in some code refactoring. Affects only PIDE based code.
2015-02-11Fixing bug #4019, and checker blow-up at once.Pierre-Marie Pédrot
2015-02-11Clarifying the implementation of universe hashconsing.Pierre-Marie Pédrot
2015-02-11Adding a statistic function on hashconsing tables.Pierre-Marie Pédrot
2015-02-11Tactic Notation: use stable unique key for notations (Close: 3970)Enrico Tassi
This is a fixup of commit 2e09a22b that used uniquely generated kernel names but forgot to substitute them.
2015-02-11Adding a test-suite for tactic notation naming.Pierre-Marie Pédrot
2015-02-11Make coqdoc -l properly handle Local before Ltac. (Fix for bug #3307)Guillaume Melquiond
2015-02-11Adding test for bug #3900.Pierre-Marie Pédrot
2015-02-11Fixing bug #3900.Pierre-Marie Pédrot
2015-02-11Reinstauring backtrace display in CoqIDE.Pierre-Marie Pédrot
2015-02-10Avoid html markup inside tex files and fix url.Guillaume Melquiond
2015-02-10Run coqdoc on the .v files from the plugins directory. (Fix for bug #2195)Guillaume Melquiond
2015-02-10Fixing #4001 (missing type constraints when building return clause of match).Hugo Herbelin
2015-02-10Improving further e11854569b8 and 3e5b9ab9f75e4 on when to print goals in ↵Hugo Herbelin
coqtop mode.
2015-02-10Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ↵Hugo Herbelin
declarations).
2015-02-10Fixing #4018 (uncaught exception on non-equality in intros [=]).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 04:30:34 +0000