aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Opaqueproofs: sink futures when interactiveGravatar Enrico Tassi2014-04-25
* print futures in caml toplevel tooGravatar Enrico Tassi2014-04-25
* Fix a second, trickier, typo in Termops.eta_reduce_head.Gravatar Arnaud Spiwack2014-04-25
* Adding a debug printer for futures.Gravatar Pierre-Marie Pédrot2014-04-25
* Fixing various backtrace recordings.Gravatar Pierre-Marie Pédrot2014-04-25
* Fix a small typo in Termops.eta_reduce_head.Gravatar Arnaud Spiwack2014-04-25
* Adding a [fold_map] operation on constrs.Gravatar Pierre-Marie Pédrot2014-04-24
* Writing tclABSTRACT in the new monad. In particular the unsafe status is nowGravatar Pierre-Marie Pédrot2014-04-24
* Better representation of evar filters: we represent the vacuous filters ofGravatar Pierre-Marie Pédrot2014-04-23
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Import proof of decidability of negated formulas from Coquelicot.Gravatar Guillaume Melquiond2014-04-23
* Remove some uses of excluded middle.Gravatar Guillaume Melquiond2014-04-22
* Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from Co...Gravatar Guillaume Melquiond2014-04-22
* Add regression tests for 3188 and 3265Gravatar Jason Gross2014-04-22
* Removing the compatibility layer from Leminv. Also removed an undocumentedGravatar Pierre-Marie Pédrot2014-04-22
* Using the new monad tactic in Inv.Gravatar Pierre-Marie Pédrot2014-04-22
* Removing tactic compatibility layer from Elim.Gravatar Pierre-Marie Pédrot2014-04-22
* Small code cleaning in Tacticals.Gravatar Pierre-Marie Pédrot2014-04-22
* Simplifying interface of elimination tactics. They used dummy clausenvs, andGravatar Pierre-Marie Pédrot2014-04-22
* Adding a test for bug #2923.Gravatar Pierre-Marie Pédrot2014-04-20
* Adding a test for bug #3285.Gravatar Pierre-Marie Pédrot2014-04-20
* Fixing bug #3285.Gravatar Pierre-Marie Pédrot2014-04-20
* Adding a [map] primitive to the tactic monad. Hopefully this should beGravatar Pierre-Marie Pédrot2014-04-20
* Fixing missing headers.Gravatar Hugo Herbelin2014-04-16
* Closing bug #3260Gravatar Julien Forest2014-04-14
* Fix guard condition for nested cofixpoints in checker.Gravatar Maxime Dénès2014-04-10
* Fix guard condition for nested cofixpoints.Gravatar Maxime Dénès2014-04-10
* better description of bug 3251Gravatar Enrico Tassi2014-04-10
* Have the feedback bus as a backend for dumping globs.Gravatar Carst Tankink2014-04-10
* Dumpglob: factor out reference dumping.Gravatar Carst Tankink2014-04-10
* CoqIDE: options for syntax highlightingGravatar Enrico Tassi2014-04-10
* CoqIDE: removing a timer may raise an exceptionGravatar Enrico Tassi2014-04-10
* coqtop -batch refuses Back 1 but accepts Undo.Gravatar Pierre Boutillier2014-04-10
* By resolution of the CoqWG, instantiate must not be used now that refine worksGravatar Pierre Boutillier2014-04-10
* No more Coersion in Init.Gravatar Pierre Boutillier2014-04-10
* Define [projT3] and [proj3_sig]Gravatar Jason Gross2014-04-10
* Test case for bug 3037Gravatar Jason Gross2014-04-10
* Test case for 3164Gravatar Jason Gross2014-04-10
* Test case for bug 3262Gravatar Jason Gross2014-04-10
* Test case for bug #3217Gravatar Jason Gross2014-04-10
* 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
* Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with...Gravatar Pierre Boutillier2014-04-09
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-27 09:41:17 +0000