aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-04-22Using the new monad tactic in Inv.Pierre-Marie Pédrot
2014-04-22Removing tactic compatibility layer from Elim.Pierre-Marie Pédrot
2014-04-22Small code cleaning in Tacticals.Pierre-Marie Pédrot
2014-04-22Simplifying interface of elimination tactics. They used dummy clausenvs, andPierre-Marie Pédrot
that should be changed anyway.
2014-04-20Adding a test for bug #2923.Pierre-Marie Pédrot
2014-04-20Adding a test for bug #3285.Pierre-Marie Pédrot
2014-04-20Fixing bug #3285.Pierre-Marie Pédrot
2014-04-20Adding a [map] primitive to the tactic monad. Hopefully this should bePierre-Marie Pédrot
slightly more efficient in general.
2014-04-16Fixing missing headers.Hugo Herbelin
2014-04-14Closing bug #3260Julien Forest
adding a new grammar entry for clauses
2014-04-10Fix guard condition for nested cofixpoints in checker.Maxime Dénès
2014-04-10Fix guard condition for nested cofixpoints.Maxime Dénès
There were actually two problems, one of them being clearly unsound. To make sure that this does not show up somewhere else in the code, it would be better to resort to an abstraction keeping in sync the environment and the De Bruijn index of the current cofixpoints, like guard_env does for fixpoints.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 09:42:30 +0000