aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* Add a regression test for bug 3001Gravatar Jason Gross2014-04-10
|
* Add another critical bug to the test-suite.Gravatar Maxime Dénès2014-04-09
| | | | I have a fix, I'm reviewing it because there may be other bugs around.
* Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps ↵Gravatar Pierre Boutillier2014-04-09
| | | | | | | | | with -R. (Fix for Rocq/Rational.)" This reverts commit 7d3ce4012a53b123dac95381bf46aac65f865d69. Conflicts: CHANGES
* Adapt coq_makefile build rules to new -R -I semanticGravatar Pierre Boutillier2014-04-09
|
* Adapt test-suite to -I is ML onlyGravatar Pierre Boutillier2014-04-09
|
* Fix exponential behavior in native compiler with retroknowledge.Gravatar Maxime Dénès2014-04-09
|
* Fix name of some Int31 operations in native compiler.Gravatar Maxime Dénès2014-04-09
|
* Removing handshake from Spawn. It used marshalling, which is bad forGravatar Pierre-Marie Pédrot2014-04-09
| | | | non-ML applications. Control channel can be also ignored.
* nanoPG: when the cursor moves, scroll to make it appear on screenGravatar Enrico Tassi2014-04-09
|
* nanoPG: takeover keypress only when text view has focusGravatar Enrico Tassi2014-04-09
|
* Optimizing Int31 support in native compiler, by not taggingGravatar Maxime Dénès2014-04-09
| | | | applications of I31 constructor as lazy.
* Int31 decompilation in native compiler was still partial. Now fixed.Gravatar Maxime Dénès2014-04-09
|
* Machine arithmetic operations for native compiler.Gravatar Maxime Dénès2014-04-09
| | | | | This completes the port of the native compiler to retroknowledge. However, some testing and optimizations are still to be done.
* Readback for int31 values from native compiler.Gravatar Maxime Dénès2014-04-09
|
* Full support for int31 values in native compiler.Gravatar Maxime Dénès2014-04-09
|
* Partial support for open terms in int31.Gravatar Maxime Dénès2014-04-09
|
* Had to split Nativelambda in two files because of RetroknowledgeGravatar Maxime Dénès2014-04-09
| | | | dependencies.
* Int31 literals in native compiler.Gravatar Maxime Dénès2014-04-09
|
* Uint31 support.Gravatar Maxime Dénès2014-04-09
|
* Add an option -Q (tentative name).Gravatar Guillaume Melquiond2014-04-08
| | | | | | 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.
* Fix universe handling (bug introduced in vi2vo commit)Gravatar Enrico Tassi2014-04-08
| | | | | | | | | | 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.
* printer for coqchkGravatar Enrico Tassi2014-04-08
|
* Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. ↵Gravatar Guillaume Melquiond2014-04-07
| | | | (Fix for Rocq/Rational.)
* Allowing proof view to be detached in CoqIDE.Gravatar Pierre-Marie Pédrot2014-04-07
|
* Transfering the initial goals from the proofview to the proof object.Gravatar Pierre-Marie Pédrot2014-04-07
| | | | They were just passed along in the tactics.
* Removing unused functions in Refiner.Gravatar Pierre-Marie Pédrot2014-04-06
|
* Actually using the [modify] primitive.Gravatar Pierre-Marie Pédrot2014-04-06
|
* Adding an [modify] function to the tactic monad. It allows to modifyGravatar Pierre-Marie Pédrot2014-04-06
| | | | the current state without having to use both get, bind and set.
* Add tool for fully qualifying Require statements.Gravatar Guillaume Melquiond2014-04-06
|
* Change handling of loadpath and mlpath.Gravatar Guillaume Melquiond2014-04-06
| | | | | | | | | | | | | - 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.
* Completing text of the question on conservativity of CIC over CC (bug #2697).Gravatar Hugo Herbelin2014-04-05
|
* Test for bug #3142, actually duplicate of #3262.Gravatar Hugo Herbelin2014-04-05
|
* Fixing bug #3228 (fixing precedence of ltac variables over variables in env).Gravatar Hugo Herbelin2014-04-05
|
* Printers for ltac environments.Gravatar Hugo Herbelin2014-04-05
|
* closing bug 3037Gravatar Julien Forest2014-04-05
|
* Fix for bug #3107.Gravatar Guillaume Melquiond2014-04-04
|
* fixing Function docGravatar Julien Forest2014-04-04
|
* Recognize "Instance" in coqwc. (Fix for bug #2551)Gravatar Guillaume Melquiond2014-04-04
|
* Closing bug #3164Gravatar Julien Forest2014-04-04
|
* Prevent verbatim text from leaking out of comments. (See bug #2882)Gravatar Guillaume Melquiond2014-04-04
|
* Fixing coqchk. It was my fault, I misused canonical and user equalitiesGravatar Pierre-Marie Pédrot2014-04-04
| | | | | when defining cache hash tables in Closure. Why it was working in 3.12 is a mystery to me.
* Fixing #3262 which revealed a non-progressing, hence looping,Gravatar Hugo Herbelin2014-04-04
| | | | | | | refinement of evars (in filter_candidates). Incidentally introduced a copy of type "option", "update", which highlights the specific intention of "updating" or not.
* Support other forms of "Proof" in coqwc. (Fix for bug #2735)Gravatar Guillaume Melquiond2014-04-04
|
* Remove option -g as it is non-portable yet does not have any effect on the ↵Gravatar Guillaume Melquiond2014-04-04
| | | | test-suite. (Fix for bug #3024)
* Clean up the .merlinGravatar Thomas Refis2014-04-03
| | | | | | | | | | | | | | | | | | | | | | | | | 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.
* A debug printer for Evd.Filter.tGravatar Pierre Boutillier2014-04-02
|
* Add a test case for bug 3251Gravatar Jason Gross2014-04-02
| | | | It was closed in 5b39c3535f7b3383d89d7b844537244a4e7c0eca.
* STM: be more resilient to explicit Back + Sideff commands (closes: 3251)Gravatar Enrico Tassi2014-04-02
|
* Fix Bug 3131 + Really drop mentions of info in refman.Gravatar Pierre Boutillier2014-04-02
|
* Fix Bug 3217Gravatar Pierre Boutillier2014-04-02
| | | | | Normalize the term to see if there are arguments to daclare implicits only if at least one argument occurs in the non normal form
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 18:29:14 +0000