aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* 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
* In Show Universes, print universes before normalization.Gravatar Matthieu Sozeau2015-01-05
* Updating documentation about bullets.Gravatar Pierre Courtieu2015-01-05
* Removing GUtil dependency from ide/document.ml.Gravatar Pierre-Marie Pédrot2015-01-05
* Adding an option to deactivate the progress bar.Gravatar Pierre-Marie Pédrot2015-01-05
* Implementing a segment-viewer in CoqIDE.Gravatar Pierre-Marie Pédrot2015-01-05
* STM: Make assert unneeded (Close 3898)Gravatar Enrico Tassi2015-01-04
* Adapting two files from test-suite to now forbidden Require's in modules.Gravatar Hugo Herbelin2015-01-04
* Fixing 48509b61 which improved unification as expected but actuallyGravatar Hugo Herbelin2015-01-03
* Fixing #3896 (incorrect sigma given to printer).Gravatar Hugo Herbelin2015-01-03
* Tentatively trying to restore the use of second-order typed-basedGravatar Hugo Herbelin2015-01-03
* Fixing #3895 (thanks to PMP for diagnosis).Gravatar Hugo Herbelin2015-01-03
* An optimization in the use of unification candidates so as to get theGravatar Hugo Herbelin2015-01-01
* Document the new behavior of lazymatch.Gravatar Guillaume Melquiond2014-12-30
* Fixing #3892: Ensure that notation variables do not capture namesGravatar Hugo Herbelin2014-12-30
* Simplifying second_order_matching: no need to invert the linearGravatar Hugo Herbelin2014-12-30
* Compatibility ocaml 3.12.Gravatar Hugo Herbelin2014-12-30
* more CHANGESGravatar Enrico Tassi2014-12-30
* Minor fixes for the win32 installerGravatar Enrico Tassi2014-12-30
* Fixing bug #3632 for good.Gravatar Pierre-Marie Pédrot2014-12-29
* Proof using: do not clear letins (unless they use a cleared var)Gravatar Enrico Tassi2014-12-29
* Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ...Gravatar Arnaud Spiwack2014-12-28
* Call nf_constraints also when compiling directly to voGravatar Enrico Tassi2014-12-28
* Proof using: call "clear" to remove from sight the vars not selectedGravatar Enrico Tassi2014-12-28
* remove debug prints (leftover)Gravatar Enrico Tassi2014-12-28
* STM: check with the kernel proof terms on the worker tooGravatar Enrico Tassi2014-12-27
* STM: fix processing of errorsGravatar Enrico Tassi2014-12-27
* STM: module Pp is openGravatar Enrico Tassi2014-12-27
* proof_global: make it possible to call close_proof in a workerGravatar Enrico Tassi2014-12-27
* include test-suite/coqchk in the summary logGravatar Enrico Tassi2014-12-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 17:43:05 +0000