coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| *	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
* \|	Splitting kernel universe code in two modules.	Pierre-Marie Pédrot	2015-10-06
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-06
\|\\|
\| *	Fixing emacs output in debugging mode.	Pierre Courtieu	2015-10-06
\| *	Univs (pretyping): call vm_compute/native_compute with the current	Matthieu Sozeau	2015-10-06
\| *	Fix bug #4354: interpret hints in the right env and sigma.	Matthieu Sozeau	2015-10-06
\| *	Univs: fix bug #4288, Print Sorted generated backward < constraints.	Matthieu Sozeau	2015-10-05
\| *	Univs: fix printing bug #3797.	Matthieu Sozeau	2015-10-05
\| *	Update the .mailmap file.	Guillaume Melquiond	2015-10-05
\| *	Univs: fix handling of evar_map in identity coercion construction.	Matthieu Sozeau	2015-10-05
\| *	Fix typo. (Fix bug #4355)	Guillaume Melquiond	2015-10-04
\| *	Mark the Coq.Compat files for documentation. (Fix bug #4353)	Guillaume Melquiond	2015-10-02
\| *	Updating versions history with data from Gérard.	Hugo Herbelin	2015-10-02
\| *	Fixing error messages about Hint.	Hugo Herbelin	2015-10-02
\| *	Improving reference manual in that auto uses simple apply rather than apply.	Hugo Herbelin	2015-10-02
\| *	Update the history of versions with recent versions.	Hugo Herbelin	2015-10-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\\|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-02
\|\ \
\| \| *	Univs: Change intf of push_named_def to return the computed universe	Matthieu Sozeau	2015-10-02
\| \| *	Univs: refined handling of assumptions	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix checker generating undeclared universes.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix test-suite file for #4287, now properly rejected.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: Remove test-suite file #3309	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix test-suite file (4301 is invalid, but a good regression test)	Matthieu Sozeau	2015-10-02
\| \| *	Fix after rebase...	Matthieu Sozeau	2015-10-02
\| \| *	Univs: forgot a substitution in mod_typing.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: correct handling of with in modules	Matthieu Sozeau	2015-10-02
\| \| *	Univs: the stdlib now needs 5 universes	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix bug #4251, handling of template polymorphic constants.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: update checker	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fixed 3685 by side-effect :)	Matthieu Sozeau	2015-10-02
\| \| *	Univs: minor fixes to test-suite files	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix handling of evd's universes and side effects in build_by_tactic	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix semantics of Type in proof mode in universe-polymorphic mode	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix minimization to allow lowering a universe to Set, not Prop.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix inference of the lowest sort for records.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix subtyping of polymorphic parameters.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix evar_map handling in Hint processing.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix test-suite file for HoTT/coq bug #120	Matthieu Sozeau	2015-10-02
\| \| *	Univs: test-suite file for bug #2016	Matthieu Sozeau	2015-10-02
\| \| *	Univs: test-suite file for #4301, subtyping of poly parameters	Matthieu Sozeau	2015-10-02
\| \| *	Univs: uncovered bug in strengthening of opaque polymorphic definitions.	Matthieu Sozeau	2015-10-02
\| \| *	Fix test-suite file for bug #3777	Matthieu Sozeau	2015-10-02
\| \| *	Fix test-suite file: failing earlier as expected.	Matthieu Sozeau	2015-10-02
\| \| *	Fix test-suite file	Matthieu Sozeau	2015-10-02
\| \| *	Univs: correcly compute the levels of records when they fall in Prop.	Matthieu Sozeau	2015-10-02
\| \| *	Univs/program: handle side effects in obligations.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix Show Universes.	Matthieu Sozeau	2015-10-02
\| \| *	Univs: fix handling of side effects/delayed proofs	Matthieu Sozeau	2015-10-02
\| \| *	Univs: handle side-effects of futures correctly in kernel.	Matthieu Sozeau	2015-10-02