aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* improve efficiency of the reduction interpreter of the checkerGravatar Bruno Barras2015-01-06
* Fixing test for bug #2830.Gravatar Pierre-Marie Pédrot2015-01-06
* Rename ill-named "imports" field of safe_env into "required".Gravatar Maxime Dénès2015-01-06
* Propagating the relaxing of filtering started in 48509b6, fixed inGravatar Hugo Herbelin2015-01-06
* Fixing old filter bug in second_order_matching.Gravatar Hugo Herbelin2015-01-06
* Added more informative messages about bullets.Gravatar Pierre Courtieu2015-01-05
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 19:32:12 +0000