aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-04-10better description of bug 3251Enrico Tassi
2014-04-10Have the feedback bus as a backend for dumping globs.Carst Tankink
2014-04-10Dumpglob: factor out reference dumping.Carst Tankink
Factored out all functions that dump references to use one function "dump_ref"
2014-04-10CoqIDE: options for syntax highlightingEnrico Tassi
2014-04-10CoqIDE: removing a timer may raise an exceptionEnrico Tassi
2014-04-10coqtop -batch refuses Back 1 but accepts Undo.Pierre Boutillier
2014-04-10By resolution of the CoqWG, instantiate must not be used now that refine worksPierre Boutillier
2014-04-10No more Coersion in Init.Pierre Boutillier
2014-04-10Define [projT3] and [proj3_sig]Jason Gross
Also allow [projT1]/[projT2] to work for [sigT2]s and [proj1_sig]/[proj2_sig] to work for [sig2]s, by means of coercions. This closes Bug 3044. This closes Pull Request #4.
2014-04-10Test case for bug 3037Jason Gross
Closed in 4a8950ec7a0d9f2b216e67e69b446c064590a8e9
2014-04-10Test case for 3164Jason Gross
Closed in 69c4d0fd7b8325187e8da697a9c283594047d. I used [Timeout 2] to distinguish between stack overflow and immediate return.
2014-04-10Test case for bug 3262Jason Gross
Closed in f65fa9de8a4c9c12d933188a755b51508bd51921 I used [Timeout 2 Fail] to test the difference between immediate failure and stack overflow. Hopefully this is robust enough.
2014-04-10Test case for bug #3217Jason Gross
It was fixed in c3feef4ed5dec126f1144dec91eee9c0f0522a94. The test case uses [Timeout 2] to test for "Coq runs instantaneously rather than running out of memory". Hopefully this is robust enough.
2014-04-10Add a regression test for bug 3001Jason Gross
2014-04-09Add 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-09Revert "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-09Adapt coq_makefile build rules to new -R -I semanticPierre Boutillier
2014-04-09Adapt test-suite to -I is ML onlyPierre Boutillier
2014-04-09Fix exponential behavior in native compiler with retroknowledge.Maxime Dénès
2014-04-09Fix name of some Int31 operations in native compiler.Maxime Dénès
2014-04-09Removing handshake from Spawn. It used marshalling, which is bad forPierre-Marie Pédrot
non-ML applications. Control channel can be also ignored.
2014-04-09nanoPG: when the cursor moves, scroll to make it appear on screenEnrico Tassi
2014-04-09nanoPG: takeover keypress only when text view has focusEnrico Tassi
2014-04-09Optimizing Int31 support in native compiler, by not taggingMaxime Dénès
applications of I31 constructor as lazy.
2014-04-09Int31 decompilation in native compiler was still partial. Now fixed.Maxime Dénès
2014-04-09Machine 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-09Readback for int31 values from native compiler.Maxime Dénès
2014-04-09Full support for int31 values in native compiler.Maxime Dénès
2014-04-09Partial support for open terms in int31.Maxime Dénès
2014-04-09Had to split Nativelambda in two files because of RetroknowledgeMaxime Dénès
dependencies.
2014-04-09Int31 literals in native compiler.Maxime Dénès
2014-04-09Uint31 support.Maxime Dénès
2014-04-08Add 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-08Fix 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-08printer for coqchkEnrico Tassi
2014-04-07Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. ↵Guillaume Melquiond
(Fix for Rocq/Rational.)
2014-04-07Allowing proof view to be detached in CoqIDE.Pierre-Marie Pédrot
2014-04-07Transfering the initial goals from the proofview to the proof object.Pierre-Marie Pédrot
They were just passed along in the tactics.
2014-04-06Removing unused functions in Refiner.Pierre-Marie Pédrot
2014-04-06Actually using the [modify] primitive.Pierre-Marie Pédrot
2014-04-06Adding an [modify] function to the tactic monad. It allows to modifyPierre-Marie Pédrot
the current state without having to use both get, bind and set.
2014-04-06Add tool for fully qualifying Require statements.Guillaume Melquiond
2014-04-06Change 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-05Completing text of the question on conservativity of CIC over CC (bug #2697).Hugo Herbelin
2014-04-05Test for bug #3142, actually duplicate of #3262.Hugo Herbelin
2014-04-05Fixing bug #3228 (fixing precedence of ltac variables over variables in env).Hugo Herbelin
2014-04-05Printers for ltac environments.Hugo Herbelin
2014-04-05closing bug 3037Julien Forest
2014-04-04Fix for bug #3107.Guillaume Melquiond
2014-04-04fixing Function docJulien Forest
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 16:47:32 +0000