coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-26
\|\\|
\| *	Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331)	Pierre Letouzey	2015-10-25
\| *	Minor module cleanup : error HigherOrderInclude was never happening	Pierre Letouzey	2015-10-25
\| *	Fixing a bug in reporting ill-formed inductive.	Hugo Herbelin	2015-10-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-19
\|\\|
\| *	Miscellaneous typos, spacing, US spelling in comments or variable names.	Hugo Herbelin	2015-10-18
\| *	Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,	Hugo Herbelin	2015-10-18
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-10-16
\|\\|
* \|	Hashcons bytecode generated by the VM.	Pierre-Marie Pédrot	2015-10-16
* \|	Exporting a purely functional interface to bytecode patching.	Pierre-Marie Pédrot	2015-10-16
\| *	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