| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-04-10 | Add a regression test for bug 3001 | Jason Gross | |
| 2014-04-09 | Add another critical bug to the test-suite. | Maxime Dénès | |
| I have a fix, I'm reviewing it because there may be other bugs around. | |||
| 2014-04-09 | Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps ↵ | Pierre Boutillier | |
| with -R. (Fix for Rocq/Rational.)" This reverts commit 7d3ce4012a53b123dac95381bf46aac65f865d69. Conflicts: CHANGES | |||
| 2014-04-09 | Adapt coq_makefile build rules to new -R -I semantic | Pierre Boutillier | |
| 2014-04-09 | Adapt test-suite to -I is ML only | Pierre Boutillier | |
| 2014-04-09 | Fix exponential behavior in native compiler with retroknowledge. | Maxime Dénès | |
| 2014-04-09 | Fix name of some Int31 operations in native compiler. | Maxime Dénès | |
| 2014-04-09 | Removing handshake from Spawn. It used marshalling, which is bad for | Pierre-Marie Pédrot | |
| non-ML applications. Control channel can be also ignored. | |||
| 2014-04-09 | nanoPG: when the cursor moves, scroll to make it appear on screen | Enrico Tassi | |
| 2014-04-09 | nanoPG: takeover keypress only when text view has focus | Enrico Tassi | |
| 2014-04-09 | Optimizing Int31 support in native compiler, by not tagging | Maxime Dénès | |
| applications of I31 constructor as lazy. | |||
| 2014-04-09 | Int31 decompilation in native compiler was still partial. Now fixed. | Maxime Dénès | |
| 2014-04-09 | Machine arithmetic operations for native compiler. | Maxime Dénès | |
| This completes the port of the native compiler to retroknowledge. However, some testing and optimizations are still to be done. | |||
| 2014-04-09 | Readback for int31 values from native compiler. | Maxime Dénès | |
| 2014-04-09 | Full support for int31 values in native compiler. | Maxime Dénès | |
| 2014-04-09 | Partial support for open terms in int31. | Maxime Dénès | |
| 2014-04-09 | Had to split Nativelambda in two files because of Retroknowledge | Maxime Dénès | |
| dependencies. | |||
| 2014-04-09 | Int31 literals in native compiler. | Maxime Dénès | |
| 2014-04-09 | Uint31 support. | Maxime Dénès | |
| 2014-04-08 | Add an option -Q (tentative name). | Guillaume Melquiond | |
| This option complements -I-as and -R. As the two other options, it adds a new loadpath, but contrarily to them, files are not looked into the directory unless fully qualified. | |||
| 2014-04-08 | Fix universe handling (bug introduced in vi2vo commit) | Enrico Tassi | |
| Inside a section, Let followed by a Proof. Qed. are handled as regular definitions, hence they have universe constraints coming from the type and from the body. Only the former set was returned to libstack, but both sets were added to the global universe graph. Hence, at section closing time, an incomplete set of universe constraints was added back to the global graph (End Section replays the libstack) and hence saved in the .vo file. coqchk was right in reporting missing constraints. | |||
| 2014-04-08 | printer for coqchk | Enrico Tassi | |
| 2014-04-07 | Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. ↵ | Guillaume Melquiond | |
| (Fix for Rocq/Rational.) | |||
| 2014-04-07 | Allowing proof view to be detached in CoqIDE. | Pierre-Marie Pédrot | |
| 2014-04-07 | Transfering the initial goals from the proofview to the proof object. | Pierre-Marie Pédrot | |
| They were just passed along in the tactics. | |||
| 2014-04-06 | Removing unused functions in Refiner. | Pierre-Marie Pédrot | |
| 2014-04-06 | Actually using the [modify] primitive. | Pierre-Marie Pédrot | |
| 2014-04-06 | Adding an [modify] function to the tactic monad. It allows to modify | Pierre-Marie Pédrot | |
| the current state without having to use both get, bind and set. | |||
| 2014-04-06 | Add tool for fully qualifying Require statements. | Guillaume Melquiond | |
| 2014-04-06 | Change handling of loadpath and mlpath. | Guillaume Melquiond | |
| - Option -I no longer handles loadpath, only mlpath. This is the same behavior as coq_makefile. Option -I-as is unchanged. - Option -R no longer recursively adds to mlpath; only the root directory is added. - user-contrib/ and xdg directories are no longer recursively added to the loadpath. - theories/ and plugins/ are no longer recursively added to the loadpath when option -nois is passed. - All the preconfigured directories are still recursively added to the mlpath though. | |||
| 2014-04-05 | Completing text of the question on conservativity of CIC over CC (bug #2697). | Hugo Herbelin | |
| 2014-04-05 | Test for bug #3142, actually duplicate of #3262. | Hugo Herbelin | |
| 2014-04-05 | Fixing bug #3228 (fixing precedence of ltac variables over variables in env). | Hugo Herbelin | |
| 2014-04-05 | Printers for ltac environments. | Hugo Herbelin | |
| 2014-04-05 | closing bug 3037 | Julien Forest | |
| 2014-04-04 | Fix for bug #3107. | Guillaume Melquiond | |
| 2014-04-04 | fixing Function doc | Julien Forest | |
| 2014-04-04 | Recognize "Instance" in coqwc. (Fix for bug #2551) | Guillaume Melquiond | |
| 2014-04-04 | Closing bug #3164 | Julien Forest | |
| 2014-04-04 | Prevent verbatim text from leaking out of comments. (See bug #2882) | Guillaume Melquiond | |
| 2014-04-04 | Fixing coqchk. It was my fault, I misused canonical and user equalities | Pierre-Marie Pédrot | |
| when defining cache hash tables in Closure. Why it was working in 3.12 is a mystery to me. | |||
| 2014-04-04 | Fixing #3262 which revealed a non-progressing, hence looping, | Hugo Herbelin | |
| refinement of evars (in filter_candidates). Incidentally introduced a copy of type "option", "update", which highlights the specific intention of "updating" or not. | |||
| 2014-04-04 | Support other forms of "Proof" in coqwc. (Fix for bug #2735) | Guillaume Melquiond | |
| 2014-04-04 | Remove option -g as it is non-portable yet does not have any effect on the ↵ | Guillaume Melquiond | |
| test-suite. (Fix for bug #3024) | |||
| 2014-04-03 | Clean up the .merlin | Thomas Refis | |
| I added a .merlin in ide/ who inherits everything from the root .merlin and also adds the dependency to lablgtk, which I removed from the root file. These way people not working on that part of the code won't get bothered if they don't have that package. I removed the S/B entry for plugins which was useless, indeed there is no ML file in that directory and merlin doesn't scan the subdirectories recursively (as you know). I also removed the S/B entry for checker since most of the files of this directory are also present in kernel and that was the cause of a lot errors on merlin's side (think "inconsistent assumptions"). On top of that, no part of the tree depends on checker (I back that assertion by a grep of the *.d files of the tree) so these lines in the .merlin were actually useless. The only part of the tree where you need to know what's in checker/ is when you are working in checker/ itself, but since merlin automatically adds the directory of the file under edition in its source and load paths nothing else is needed. There might still be problems after this patch, but they should be less of them. Considering my poor knowledge of the codebase there might be other conflicts I have missed. | |||
| 2014-04-02 | A debug printer for Evd.Filter.t | Pierre Boutillier | |
| 2014-04-02 | Add a test case for bug 3251 | Jason Gross | |
| It was closed in 5b39c3535f7b3383d89d7b844537244a4e7c0eca. | |||
| 2014-04-02 | STM: be more resilient to explicit Back + Sideff commands (closes: 3251) | Enrico Tassi | |
| 2014-04-02 | Fix Bug 3131 + Really drop mentions of info in refman. | Pierre Boutillier | |
| 2014-04-02 | Fix Bug 3217 | Pierre Boutillier | |
| Normalize the term to see if there are arguments to daclare implicits only if at least one argument occurs in the non normal form | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |