aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-04-25print futures in caml toplevel tooEnrico Tassi
2014-04-25Fix a second, trickier, typo in Termops.eta_reduce_head.Arnaud Spiwack
2014-04-25Adding a debug printer for futures.Pierre-Marie Pédrot
2014-04-25Fixing various backtrace recordings.Pierre-Marie Pédrot
2014-04-25Fix a small typo in Termops.eta_reduce_head.Arnaud Spiwack
2014-04-24Adding a [fold_map] operation on constrs.Pierre-Marie Pédrot
2014-04-24Writing tclABSTRACT in the new monad. In particular the unsafe status is nowPierre-Marie Pédrot
preserved.
2014-04-23Better representation of evar filters: we represent the vacuous filters ofPierre-Marie Pédrot
any length with a [None] representation and ensure that this representation is canonical through the restricted interface.
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-23Import proof of decidability of negated formulas from Coquelicot.Guillaume Melquiond
2014-04-22Remove some uses of excluded middle.Guillaume Melquiond
2014-04-22Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from ↵Guillaume Melquiond
Coquelicot. This change removes the need for excluded middle. It also greatly simplifies the proof (no need for geometric series, limits, constructive epsilon, and so on).
2014-04-22Add regression tests for 3188 and 3265Jason Gross
2014-04-22Removing the compatibility layer from Leminv. Also removed an undocumentedPierre-Marie Pédrot
variant of the Derive Inversion command which took the current goal as the targeted inductive. It was unused in the contribs and it seemed rather bad from the STM point of view, as it generated a lemma inside a proof.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 01:24:50 +0000