| Age | Commit message (Expand) | Author |
|---|
| 2017-05-30 | Makefile: no bytecode compilation in make world, see make byte instead | Pierre Letouzey |
| 2017-05-30 | Merge PR#693: A subtle bug in tclWITHHOLES. | Maxime Dénès |
| 2017-05-30 | [readlink -f] doesn't work on OSX | Gaëtan Gilbert |
| 2017-05-30 | Support for using type information to infer more precise evar sources. | Hugo Herbelin |
| 2017-05-30 | Merge PR#695: Omega: fix bug #4132 | Maxime Dénès |
| 2017-05-30 | Documentation for eassert, eenough, epose proof, eset, eremember, epose. | Hugo Herbelin |
| 2017-05-30 | Few tests for e-variants of assert, set, remember. | Hugo Herbelin |
| 2017-05-30 | Adding "epose", "eset", "eremember" which allow to set terms with | Hugo Herbelin |
| 2017-05-30 | Adding "eassert", "eenough", "epose proof", which allow to state | Hugo Herbelin |
| 2017-05-30 | make sure that "ocamllibdep" properly recognizes Ocaml modules that are all u... | Matej Košík |
| 2017-05-30 | Fix bug 5550: "typeclasses eauto with" does not work with section variables. | Théo Zimmermann |
| 2017-05-30 | Merge PR#356: Making management of installation directories more structured, ... | Maxime Dénès |
| 2017-05-30 | cleanup in ".merlin" file | Matej Kosik |
| 2017-05-30 | make the expansion of the "DECLARE PLUGIN" closer to the way how a human woul... | Matej Kosik |
| 2017-05-30 | Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3 | Maxime Dénès |
| 2017-05-29 | Merge PR#687: Gitlab CI | Maxime Dénès |
| 2017-05-29 | Pretyping cleanup: remove constr_of_global calls | Matthieu Sozeau |
| 2017-05-29 | tactics cleanup: remove constr_of_global calls | Matthieu Sozeau |
| 2017-05-29 | Omega: use "simpl" only on coefficents, not on atoms (fix #4132) | Pierre Letouzey |
| 2017-05-29 | Merge PR#690: [stm] Uniformize `Sideff / Sideff. | Maxime Dénès |
| 2017-05-29 | Ltac cleanup: no more constr_of_global calls | Matthieu Sozeau |
| 2017-05-29 | Equality cleanup: remove constr_of_global | Matthieu Sozeau |
| 2017-05-29 | Command.ml cleanup: remove constr_of_global calls | Matthieu Sozeau |
| 2017-05-29 | Merge PR#555: Missing optimization when Kernel Term Sharing is disabled. | Maxime Dénès |
| 2017-05-29 | Configuration with -local definitively seen as an installation layout like ot... | Hugo Herbelin |
| 2017-05-29 | Using the same strategy in coqdoc than in coqtop to guess the coqlib. | Hugo Herbelin |
| 2017-05-29 | Relying on computation done in Envars to discover the installation directories. | Hugo Herbelin |
| 2017-05-29 | Generalizing to docdir and datadir the test for a relocated installation. | Hugo Herbelin |
| 2017-05-29 | Exporting the suffixes needed to build coqlib, docdir, etc. | Hugo Herbelin |
| 2017-05-29 | Using Coq_config.local rather than None to tell that Coq_config.coqlib is local. | Hugo Herbelin |
| 2017-05-29 | Cleanup: removal of constr_of_global. | Matthieu Sozeau |
| 2017-05-29 | Configure: viewing compilation in -local itself as an installation layout. | Hugo Herbelin |
| 2017-05-29 | Configuration: always giving a value to configdir and datadir. | Hugo Herbelin |
| 2017-05-29 | More structure and more code factorization in building default | Hugo Herbelin |
| 2017-05-29 | Unifying the layout of installation directories. | Hugo Herbelin |
| 2017-05-29 | Unified terminology in configure.ml/coq_config.ml: arch_win32 -> arch_is_win32. | Hugo Herbelin |
| 2017-05-29 | Mini-renaming in configure.ml to avoid switching back and forth from | Hugo Herbelin |
| 2017-05-29 | Dead code (xdg_config_dirs). | Hugo Herbelin |
| 2017-05-29 | Merge PR#685: Fix a bug in checker | Maxime Dénès |
| 2017-05-29 | Merge PR#546: Fix for bug #4499 and other minor related bugs | Maxime Dénès |
| 2017-05-29 | Merge PR#512: [cleanup] Unify all calls to the error function. | Maxime Dénès |
| 2017-05-28 | Fix a bug in checker | Amin Timany |
| 2017-05-28 | Merge PR#678: [coqlib] Move `Coqlib` to `library/`. | Maxime Dénès |
| 2017-05-28 | Merge PR#689: Changes to make coq-makefile not failing on MacOS X. | Maxime Dénès |
| 2017-05-28 | Fail on deprecated warning even for Ocaml > 4.02.3 | Gaëtan Gilbert |
| 2017-05-28 | Fixing a subtle bug in tclWITHHOLES. | Hugo Herbelin |
| 2017-05-28 | Merge PR#675: [coqlib] Deprecate redundant Coqlib functions. | Maxime Dénès |
| 2017-05-28 | Merge PR#683: coq_makefile: build .cma for each .mlpack | Maxime Dénès |
| 2017-05-28 | More uniform indentation of sigma lemmas | Jason Gross |
| 2017-05-28 | Give explicit proof terms to proj2_sig_eq etc. | Jason Gross |
