coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	Univs: fix bug #4288, Print Sorted generated backward < constraints.	Matthieu Sozeau	2015-10-05
*	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
*	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
*	Fix a bug in 31 bit arithmetic, leading to failing conversion tests.	Maxime Dénès	2015-09-06
*	Fixed critical bug in 31 bit arithmetic of VM	Catalin Hritcu	2015-09-06
*	print universes when dumping bytecode.	Gregory Malecha	2015-09-03
*	Implementing Herbelin's fix for the "NonPar" bug	mlasson	2015-09-03
*	Fixing pop_rel_context.	Hugo Herbelin	2015-08-02
*	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
*	Fixing pop_rel_context	Hugo Herbelin	2015-08-02