aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-04-23Better representation of evar filters: we represent the vacuous filters ofPierre-Marie Pédrot
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 Co...Guillaume Melquiond
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
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
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
2014-04-16Fixing missing headers.Hugo Herbelin
2014-04-14Closing bug #3260Julien Forest
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
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
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
2014-04-10Test case for bug 3037Jason Gross
2014-04-10Test case for 3164Jason Gross
2014-04-10Test case for bug 3262Jason Gross
2014-04-10Test case for bug #3217Jason Gross
2014-04-10Add a regression test for bug 3001Jason Gross
2014-04-09Add another critical bug to the test-suite.Maxime Dénès
2014-04-09Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with...Pierre Boutillier
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
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
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
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
2014-04-09Int31 literals in native compiler.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-31 04:06:02 +0000