coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Unifying betazeta_applist and prod_applist into a clearer interface.	Hugo Herbelin	2015-12-05
*	Slight simplification of the code of primitive projection (in relation	Hugo Herbelin	2015-12-05
*	Moving extended_rel_vect/extended_rel_list to the kernel.	Hugo Herbelin	2015-12-05
*	About building of substitutions from instances.	Hugo Herbelin	2015-12-05
*	Experimenting documentation of the Vars.subst functions.	Hugo Herbelin	2015-12-05
*	Contracting one extra beta-redex on the fly when typing branches of "match".	Hugo Herbelin	2015-12-05
*	A few renaming and simplification in inductive.ml.	Hugo Herbelin	2015-12-05
*	Moving three related small half-general half-ad-hoc utility functions	Hugo Herbelin	2015-12-05
*	New algorithm for universe cycle detections.	Jacques-Henri Jourdan	2015-12-01
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-29
\|\
\| *	Univs: entirely disallow instantiation of polymorphic constants with	Matthieu Sozeau	2015-11-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-26
\|\\|
\| *	Fix output of universe arcs. (Fix bug #4422)	Guillaume Melquiond	2015-11-23
\| *	Fixing kernel bug in typing match with let-ins in the arity.	Hugo Herbelin	2015-11-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-20
\|\\|
\| *	Fixing fix c71aa6b to primitive projections.	Hugo Herbelin	2015-11-18
\| *	Slightly documenting code for building primitive projections.	Hugo Herbelin	2015-11-18
\| *	Fixing logical bugs in the presence of let-ins in computiong primitive	Hugo Herbelin	2015-11-18
* \|	Hashconsing modules.	Pierre-Marie Pédrot	2015-11-15
* \|	Merge origin/v8.5 into trunk	Hugo Herbelin	2015-11-10
\|\\|
\| *	Dead code from the commit having introduced primitive projections (a4043608).	Hugo Herbelin	2015-11-10
\| *	Fixing a bug in reporting ill-formed constructor.	Hugo Herbelin	2015-11-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\|
\| *	Univs: update refman, better printers for universe contexts.	Matthieu Sozeau	2015-11-04
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-30
\|\\|
\| *	Collect subproof universes in handle_side_effects.	Matthieu Sozeau	2015-10-29
\| *	Cleanup API and comments of 908dcd613	Enrico Tassi	2015-10-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\|
\| *	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi	2015-10-28
\| *	Refine Gregory Malecha's patch on VM and universe polymorphism.	Maxime Dénès	2015-10-28
\| *	Conversion of polymorphic inductive types was incomplete in VM and native.	Maxime Dénès	2015-10-28
\| *	Fix minor typo in native compiler.	Maxime Dénès	2015-10-28
\| *	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha	2015-10-28
* \|	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
\|\\|