aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* fixup to vi -> vio renamingGravatar Enrico Tassi2015-01-12
* Whodidwhat-8.5: a global passGravatar Arnaud Spiwack2015-01-12
* whodidwhat-8.5: typo.Gravatar Arnaud Spiwack2015-01-12
* Add -no-native-compiler flag to list dumped by --help.Gravatar Maxime Dénès2015-01-12
* Add myself to credits.Gravatar Maxime Dénès2015-01-12
* Update credits.Gravatar Guillaume Melquiond2015-01-12
* Fix files in test-suite having to do with Require inside modules.Gravatar Maxime Dénès2015-01-12
* Update headers.Gravatar Maxime Dénès2015-01-12
* Update test for #3363 now that Require is forbidden inside modules.Gravatar Maxime Dénès2015-01-12
* Fix a few typos.Gravatar Maxime Dénès2015-01-12
* Fixing name of evars in output test Notation.v.Gravatar Hugo Herbelin2015-01-12
* Not "Setting ?n=?p order to ?p:=?n to see if it solves someGravatar Hugo Herbelin2015-01-12
* Fixing typo in previous commit.Gravatar Hugo Herbelin2015-01-12
* Fixing wrong duplication message when finding both a .ml and a .ml4 in coqdep.Gravatar Hugo Herbelin2015-01-11
* Avoiding a redundant information in unification error message.Gravatar Hugo Herbelin2015-01-11
* some credits for STMGravatar Enrico Tassi2015-01-11
* Extraction: discard code unnecessary to fulfill a module signatureGravatar Pierre Letouzey2015-01-11
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* Extraction: discard unnecessary code inside modules without signaturesGravatar Pierre Letouzey2015-01-11
* Extraction: no more ascii blob in type variables (fix #3227)Gravatar Pierre Letouzey2015-01-11
* Extraction : some more support functions for a future "Extraction Compute"Gravatar Pierre Letouzey2015-01-11
* Extraction: minor tweaks to ease ongoing experiments about LambdaGravatar Pierre Letouzey2015-01-11
* Adding more sharing in Map.udpate and Map.modify.Gravatar Pierre-Marie Pédrot2015-01-10
* CHANGES: mention "Optimize (Heap|Proof)"Gravatar Enrico Tassi2015-01-10
* STM: fix handling of side effects in vio2voGravatar Enrico Tassi2015-01-09
* Continuing 785f82ee1 on reverting not only f5d7b2b1e but alsoGravatar Hugo Herbelin2015-01-08
* Fixing compilation of penultimate commit d08532d.Gravatar Hugo Herbelin2015-01-08
* Setting ?n=?p order to ?p:=?n to see if it solves some incompatibilities wrt ...Gravatar Hugo Herbelin2015-01-08
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* Update + English in CHANGESGravatar Hugo Herbelin2015-01-08
* Start credits for 8.5.Gravatar Matthieu Sozeau2015-01-08
* Small fix in whodidwhat 8.5.Gravatar Pierre Courtieu2015-01-08
* Fixed and extend bullet related info/error messages. + doc.Gravatar Pierre Courtieu2015-01-08
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-08
* Add a few words in whodidwhat.Gravatar Maxime Dénès2015-01-08
* Document native_compute.Gravatar Maxime Dénès2015-01-08
* Initiating who-did-what for 8.5Gravatar Hugo Herbelin2015-01-07
* Committing whodidwhat files.Gravatar Hugo Herbelin2015-01-07
* Reverting the tentative try to restore the use of second-orderGravatar Hugo Herbelin2015-01-07
* Aligning printing of universe constraints.Gravatar Hugo Herbelin2015-01-07
* Hook when state arrives on master.Gravatar Enrico Tassi2015-01-07
* Fix checker's treatment of template polymorphicGravatar Matthieu Sozeau2015-01-06
* Safer version of the implementation of stores.Gravatar Pierre-Marie Pédrot2015-01-06
* remove unused iArrayGravatar Enrico Tassi2015-01-06
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
* Fix some documentation typos.Gravatar Guillaume Melquiond2015-01-06
* Fix setoid rewrite.Gravatar Arnaud Spiwack2015-01-06
* Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug #38...Gravatar Guillaume Melquiond2015-01-06
* updated include file for debuggingGravatar Bruno Barras2015-01-06
* improve efficiency of the reduction interpreter of coqtopGravatar Bruno Barras2015-01-06