coq - The formal proof system

Age	Commit message (Expand)	Author
2015-01-11	some credits for STM	Enrico Tassi
2015-01-11	Extraction: discard code unnecessary to fulfill a module signature	Pierre Letouzey
2015-01-11	Declarations.mli refactoring: module_type_body = module_body	Pierre Letouzey
2015-01-11	Extraction: discard unnecessary code inside modules without signatures	Pierre Letouzey
2015-01-11	Extraction: no more ascii blob in type variables (fix #3227)	Pierre Letouzey
2015-01-11	Extraction : some more support functions for a future "Extraction Compute"	Pierre Letouzey
2015-01-11	Extraction: minor tweaks to ease ongoing experiments about Lambda	Pierre Letouzey
2015-01-10	Adding more sharing in Map.udpate and Map.modify.	Pierre-Marie Pédrot
2015-01-10	CHANGES: mention "Optimize (Heap\|Proof)"	Enrico Tassi
2015-01-09	STM: fix handling of side effects in vio2vo	Enrico Tassi
2015-01-08	Continuing 785f82ee1 on reverting not only f5d7b2b1e but also	Hugo Herbelin
2015-01-08	Fixing compilation of penultimate commit d08532d.	Hugo Herbelin
2015-01-08	Setting ?n=?p order to ?p:=?n to see if it solves some incompatibilities wrt ...	Hugo Herbelin
2015-01-08	Avoiding introducing yet another convention in naming files.	Hugo Herbelin
2015-01-08	Update + English in CHANGES	Hugo Herbelin
2015-01-08	Start credits for 8.5.	Matthieu Sozeau
2015-01-08	Small fix in whodidwhat 8.5.	Pierre Courtieu
2015-01-08	Fixed and extend bullet related info/error messages. + doc.	Pierre Courtieu
2015-01-08	Fix some documentation typos.	Guillaume Melquiond
2015-01-08	Add a few words in whodidwhat.	Maxime Dénès
2015-01-08	Document native_compute.	Maxime Dénès
2015-01-07	Initiating who-did-what for 8.5	Hugo Herbelin
2015-01-07	Committing whodidwhat files.	Hugo Herbelin
2015-01-07	Reverting the tentative try to restore the use of second-order	Hugo Herbelin
2015-01-07	Aligning printing of universe constraints.	Hugo Herbelin
2015-01-07	Hook when state arrives on master.	Enrico Tassi
2015-01-06	Fix checker's treatment of template polymorphic	Matthieu Sozeau
2015-01-06	Safer version of the implementation of stores.	Pierre-Marie Pédrot
2015-01-06	remove unused iArray	Enrico Tassi
2015-01-06	rename: vi -> vio	Enrico Tassi
2015-01-06	Fix some documentation typos.	Guillaume Melquiond
2015-01-06	Fix setoid rewrite.	Arnaud Spiwack
2015-01-06	Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug #38...	Guillaume Melquiond
2015-01-06	updated include file for debugging	Bruno Barras
2015-01-06	improve efficiency of the reduction interpreter of coqtop	Bruno Barras
2015-01-06	improve efficiency of the reduction interpreter of the checker	Bruno Barras
2015-01-06	Fixing test for bug #2830.	Pierre-Marie Pédrot
2015-01-06	Rename ill-named "imports" field of safe_env into "required".	Maxime Dénès
2015-01-06	Propagating the relaxing of filtering started in 48509b6, fixed in	Hugo Herbelin
2015-01-06	Fixing old filter bug in second_order_matching.	Hugo Herbelin
2015-01-05	Added more informative messages about bullets.	Pierre Courtieu
2015-01-05	kernel/ind Change interface of declare_mind and declare_mutual	Matthieu Sozeau
2015-01-05	In Show Universes, print universes before normalization.	Matthieu Sozeau
2015-01-05	Updating documentation about bullets.	Pierre Courtieu
2015-01-05	Removing GUtil dependency from ide/document.ml.	Pierre-Marie Pédrot
2015-01-05	Adding an option to deactivate the progress bar.	Pierre-Marie Pédrot
2015-01-05	Implementing a segment-viewer in CoqIDE.	Pierre-Marie Pédrot
2015-01-04	STM: Make assert unneeded (Close 3898)	Enrico Tassi
2015-01-04	Adapting two files from test-suite to now forbidden Require's in modules.	Hugo Herbelin
2015-01-03	Fixing 48509b61 which improved unification as expected but actually	Hugo Herbelin