| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-02-16 | Documenting "induction t in ctx" when ctx contains an hyp not mentioning t. | Hugo Herbelin | |
| 2015-02-16 | Fixing bug #4035 (support for dependent destruction within ltac code). | Hugo Herbelin | |
| 2015-02-16 | Test for #2946 (trunk bug with let's in unification). | Hugo Herbelin | |
| 2015-02-16 | Fixing test for bug #3944. | Pierre-Marie Pédrot | |
| 2015-02-16 | Test for bug #3944. | Pierre-Marie Pédrot | |
| 2015-02-16 | Fixing bug #3944. | Pierre-Marie Pédrot | |
| 2015-02-15 | Fixing bug #4037. | Pierre-Marie Pédrot | |
| 2015-02-15 | Changing default for CoqIDE project to append arguments. | Pierre-Marie Pédrot | |
| Implement wish #3582. | |||
| 2015-02-15 | CoqIDE now remembers the path of the last opened project. | Pierre-Marie Pédrot | |
| Fixes bug #2762. | |||
| 2015-02-15 | Selecting whole words on double-click in CoqIDE. | Pierre-Marie Pédrot | |
| Fixes bug #4026. | |||
| 2015-02-15 | Undo: back to 8.4 semantics (Close #3514) | Enrico Tassi | |
| Only tactics are taken into account. | |||
| 2015-02-15 | Reset "section name" works again (Close #3933) | Enrico Tassi | |
| 2015-02-15 | Fix test-suite file. Check that definitions do work when sharing is | Matthieu Sozeau | |
| disabled in the kernel. | |||
| 2015-02-15 | Fix 'don't expose cases' in cbn | Pierre Boutillier | |
| 2015-02-15 | Note about "Undo. Undo." in CHANGES | Enrico Tassi | |
| 2015-02-15 | Test for bug #3490. | Pierre-Marie Pédrot | |
| 2015-02-15 | Fixing bug #3490. | Pierre-Marie Pédrot | |
| 2015-02-15 | Test for bug #3916. | Pierre-Marie Pédrot | |
| 2015-02-15 | Fixing bug #3916. | Pierre-Marie Pédrot | |
| 2015-02-15 | Fixing test-suite. | Pierre-Marie Pédrot | |
| 2015-02-15 | Document the behavior change of Instance wrt {|...|}. (Fix for bug #3749) | Guillaume Melquiond | |
| 2015-02-14 | Win: update README | Enrico Tassi | |
| 2015-02-14 | Fixing OCaml 3.12 compilation. | Pierre-Marie Pédrot | |
| 2015-02-14 | CoqIDE: restore old default colors | Enrico Tassi | |
| 2015-02-14 | typo | Enrico Tassi | |
| 2015-02-14 | Attempt to be more colorblind friendly in CoqIDE (Close #4024) | Enrico Tassi | |
| 2015-02-14 | Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior | Enrico Tassi | |
| Of course such proofs cannot be processed asynchronously | |||
| 2015-02-14 | Makefile: in byte we can always dynlink | Enrico Tassi | |
| 2015-02-14 | Test for bug #4016. | Pierre-Marie Pédrot | |
| 2015-02-14 | Fixing bug #4016. | Pierre-Marie Pédrot | |
| When setoid rewriting in a hypothesis, we push the newly introduced declaration after the last declaration it depends on. | |||
| 2015-02-14 | dependent destruction: Fix (part of) bug #3961, by fixing dependent * | Matthieu Sozeau | |
| generalizing * which was broken since 8.4. | |||
| 2015-02-14 | coqc accepts -top option. Fixes bug #4043. | Pierre-Marie Pédrot | |
| 2015-02-14 | Univs: fix bug #3755. We were missing refreshements of universes in | Matthieu Sozeau | |
| unifications ?X ~= ?Y foo not catched by solve_evar_evar. | |||
| 2015-02-14 | Univs: When computing the level of an inductive including indices, lets | Matthieu Sozeau | |
| do not contribute. Fixes bug #3808. | |||
| 2015-02-13 | Document the issue with trivial inductive types. (Workaround for bug #3984) | Guillaume Melquiond | |
| 2015-02-13 | Fixup version & copyright for MacOS bundle | Pierre Boutillier | |
| 2015-02-13 | Hardcode how coqide have to look for coqtop in MacOS bundle | Pierre Boutillier | |
| Sorry, that is ugly. Please revert if you see a better way to do it. | |||
| 2015-02-13 | Better error message for nested module application. | Maxime Dénès | |
| Fixes #3809. | |||
| 2015-02-13 | Fix test-suite file to finish | Matthieu Sozeau | |
| 2015-02-13 | Selection of the current word in CoqIDE looks at all buffers. | Pierre-Marie Pédrot | |
| 2015-02-13 | Trying 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-12 | Fixed test-suite file, that should always work. | Matthieu Sozeau | |
| 2015-02-12 | Add test-suite files for closed bugs. | Matthieu Sozeau | |
| 2015-02-12 | Tentative 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-12 | COMPATIBILITY: add note about the change of behavior of Instance foo := | Matthieu Sozeau | |
| {| |}. Add test-suite files for closed bugs. | |||
| 2015-02-12 | Univs: fix bug #4031: wrong folding of sigma in change. | Matthieu Sozeau | |
| 2015-02-12 | Univs: fix bug #3978: carry around the universe context used to | Matthieu Sozeau | |
| typecheck with definitions and thread it accordingly when typechecking module expressions. | |||
| 2015-02-12 | Fix bug #2775: Correct handling of universes in leminv. | Matthieu Sozeau | |
| 2015-02-12 | Fix typos about .vio files (thanks Arthur for spotting them) | Enrico Tassi | |
| 2015-02-12 | Fixing bug #3261. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |