coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| *	Remove left2right reference from the kernel.	Maxime Dénès	2015-10-16
\| *	Avoid dependency of the pretyper on C code.	Maxime Dénès	2015-10-15
\| *	Fix #4346 2/2: VM casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
\| *	Fix #4346 1/2: native casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
\| *	Warn user when bytecode compilation fails.	Maxime Dénès	2015-10-15
\| *	Remove now useless exception handler in default conversion.	Maxime Dénès	2015-10-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Fix detection of ties in oracle_order.	Guillaume Melquiond	2015-10-15
\| *	Univs: inductives, remove unneeded test	Matthieu Sozeau	2015-10-14
\| *	Temporary fix: kernel conversion needs to ignore l2r flag.	Maxime Dénès	2015-10-14
\| *	Remove reference to default conversion function inside the kernel.	Maxime Dénès	2015-10-14
\| *	Remove -vm flag of coqtop.	Maxime Dénès	2015-10-14
\| *	Remove unused infos structure in VM.	Maxime Dénès	2015-10-14
\| *	Make interpreter of PROJ simpler by not using the stack.	Guillaume Melquiond	2015-10-14
\| *	Remove some unused variables.	Guillaume Melquiond	2015-10-14
\| *	Fix some typos.	Guillaume Melquiond	2015-10-14
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-12
\|\\|
\| *	Univs: be more restrictive for template polymorphic constants: only	Matthieu Sozeau	2015-10-12
\| *	Gather VM tags in Cbytecodes.	Maxime Dénès	2015-10-12
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-10
\|\\|
\| *	Complete handling of primitive projections in VM.	Maxime Dénès	2015-10-09
\| *	Code cleaning in VM (with Benjamin).	Maxime Dénès	2015-10-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	Univs: fix bug #3807	Matthieu Sozeau	2015-10-08
\| *	Proof using: let-in policy, optional auto-clear, forward closure*	Enrico Tassi	2015-10-08
\| *	term_typing: strengthen discharging code	Enrico Tassi	2015-10-08
* \|	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
\|\\|
\| *	Univs: fix bug #4288, Print Sorted generated backward < constraints.	Matthieu Sozeau	2015-10-05
* \|	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: forgot a substitution in mod_typing.	Matthieu Sozeau	2015-10-02
\| *	Univs: correct handling of with in modules	Matthieu Sozeau	2015-10-02
\| *	Univs: fix bug #4251, handling of template polymorphic constants.	Matthieu Sozeau	2015-10-02
\| *	Univs: fix subtyping of polymorphic parameters.	Matthieu Sozeau	2015-10-02
\| *	Univs: uncovered bug in strengthening of opaque polymorphic definitions.	Matthieu Sozeau	2015-10-02
\| *	Univs: handle side-effects of futures correctly in kernel.	Matthieu Sozeau	2015-10-02
\| *	Univs (kernel) adapt to new invariants	Matthieu Sozeau	2015-10-02
\| *	Univs: module constraints move to universe contexts as they might	Matthieu Sozeau	2015-10-02
\| *	Forcing i > Set for global universes (incomplete)	Matthieu Sozeau	2015-10-02
\| *	Universes: enforce Set <= i for all Type occurrences.	Matthieu Sozeau	2015-10-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-09-25
\|\\|
\| *	Remove unused type_in_type field in safe_env.	Maxime Dénès	2015-09-20
\| *	Fix #3948 Anomaly: unknown constant in Print Assumptions	Maxime Dénès	2015-09-20
* \|	Better debug printers for module paths.	Maxime Dénès	2015-09-20
* \|	Remove dead code in lazy reduction machine.	Maxime Dénès	2015-09-14
* \|	Assertion checking that invariant enforced by 0f8d1b92 always holds.	Maxime Dénès	2015-09-10
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-09-06
\|\\|