aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* 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
* Optimizing Int31 support in native compiler, by not taggingGravatar Maxime Dénès2014-04-09
* Int31 decompilation in native compiler was still partial. Now fixed.Gravatar Maxime Dénès2014-04-09
* Machine arithmetic operations for native compiler.Gravatar Maxime Dénès2014-04-09
* Readback for int31 values from native compiler.Gravatar Maxime Dénès2014-04-09
* Full support for int31 values in native compiler.Gravatar Maxime Dénès2014-04-09
* Partial support for open terms in int31.Gravatar Maxime Dénès2014-04-09
* Had to split Nativelambda in two files because of RetroknowledgeGravatar Maxime Dénès2014-04-09
* Int31 literals in native compiler.Gravatar Maxime Dénès2014-04-09
* Uint31 support.Gravatar Maxime Dénès2014-04-09
* Add an option -Q (tentative name).Gravatar Guillaume Melquiond2014-04-08
* Fix universe handling (bug introduced in vi2vo commit)Gravatar Enrico Tassi2014-04-08
* printer for coqchkGravatar Enrico Tassi2014-04-08
* Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. (Fi...Gravatar Guillaume Melquiond2014-04-07
* Allowing proof view to be detached in CoqIDE.Gravatar Pierre-Marie Pédrot2014-04-07
* Transfering the initial goals from the proofview to the proof object.Gravatar Pierre-Marie Pédrot2014-04-07
* Removing unused functions in Refiner.Gravatar Pierre-Marie Pédrot2014-04-06
* Actually using the [modify] primitive.Gravatar Pierre-Marie Pédrot2014-04-06
* Adding an [modify] function to the tactic monad. It allows to modifyGravatar Pierre-Marie Pédrot2014-04-06
* Add tool for fully qualifying Require statements.Gravatar Guillaume Melquiond2014-04-06
* Change handling of loadpath and mlpath.Gravatar Guillaume Melquiond2014-04-06