coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \|	Merge branch 'v8.5' into trunk	Guillaume Melquiond	2015-12-31
\|\\| \| \|
* \| \| \|	Removing dead code.	Pierre-Marie Pédrot	2015-12-27
\| \| * \|	COMMENTS: of "Constr.case_info" type were updated.	Matej Kosik	2015-12-22
\| \| * \|	COMMENTS: added to the "Names.inductive" and "Names.constructor" types.	Matej Kosik	2015-12-22
\| \|/ / \|/\| \|
\| * \|	Inclusion of functors with restricted signature is now forbidden (fix #3746)	Pierre Letouzey	2015-12-22
* \| \|	COMMENTS: added to the "Constr.case_info" type.	Matej Kosik	2015-12-18
* \| \|	COMMENTS: added to some variants of the "Constr.kind_of_term" type.	Matej Kosik	2015-12-18
* \| \|	COMMENTS: added to the "Names" module.	Matej Kosik	2015-12-18
* \| \|	ALPHA-CONVERSION: in the "Reduction" module: clos_fconv --> clos_gen_conv	Matej Kosik	2015-12-17
* \| \|	ALPHA-CONVERSION: in the "Reduction" module: fconv --> gen_conv	Matej Kosik	2015-12-17
* \| \|	CLEANUP: in the Reduction module	Matej Kosik	2015-12-17
* \| \|	CLEANUP: in the Reduction module	Matej Kosik	2015-12-17
* \| \|	Fixing e3cefca41b about supposingly simplifying primitive projections	Hugo Herbelin	2015-12-15
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\| \|
\| * \|	bug fixes to vm computation + test cases.	Gregory Malecha	2015-12-09
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\| \|
\| * \|	Fix some typos.	Guillaume Melquiond	2015-12-07
* \| \|	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