coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix (actually, properly implement :) hashconsing of projections,	Matthieu Sozeau	2014-12-17
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Fix for #3154: use CUnix.sys_command to call native compiler.	Maxime Dénès	2014-12-16
*	Fix treatment of universe context in typecheck inductive (was added	Matthieu Sozeau	2014-12-15
*	Fix merging of name maps in union of universe contexts.	Matthieu Sozeau	2014-12-14
*	Revert commit that inverted the preference for FFlex/FProj problems in	Matthieu Sozeau	2014-12-10
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
*	Pass around information on the use of template polymorphism for	Matthieu Sozeau	2014-11-23
*	Fix #3824. de Bruijn error in normalization of fixpoints.	Maxime Dénès	2014-11-23
*	Fix bug #3804.	Matthieu Sozeau	2014-11-21
*	Exporting the function handling side-effects only applied to terms.	Pierre-Marie Pédrot	2014-11-20
*	Slightly improving error messages when mismatch with Proof using at Qed time.	Hugo Herbelin	2014-11-19
*	Option -type-in-type continued (deactivate test for inferred sort of	Hugo Herbelin	2014-11-19
*	Cleaner interfaces for linking locations of native compiler.	Maxime Dénès	2014-11-12
*	Fix #3282: VM confused by let bindings in fixpoints.	Maxime Dénès	2014-11-10
*	Better printing of dynlink errors in native compiler.	Maxime Dénès	2014-11-10
*	Fix some typos in comments.	Guillaume Melquiond	2014-10-27
*	Remove an ununsed pattern and commented code in the kernel.	Matthieu Sozeau	2014-10-24
*	Fix retroknowledge for int31 division.	Maxime Dénès	2014-10-24
*	No hash consing across calls to the native compiler.	Maxime Dénès	2014-10-24
*	Pushing Pierre's factorization of names in goal context printing from	Hugo Herbelin	2014-10-22
*	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin	2014-10-20
*	Revert "Move eta-expansion after delta reduction in kernel reduction. This ma...	Matthieu Sozeau	2014-10-14
*	selective join/export of the safe_environment	Enrico Tassi	2014-10-13
*	STM: simplify how the term part of a side effect is retrieved	Enrico Tassi	2014-10-13
*	library/opaqueTables: enable their use in interactive mode	Enrico Tassi	2014-10-13
*	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau	2014-10-11
*	Fix segfault in native compiler on int31 division.	Maxime Dénès	2014-10-10
*	Implement module subtyping for polymorphic constants (errors on	Matthieu Sozeau	2014-10-02
*	Move eta-expansion after delta reduction in kernel reduction. This makes	Matthieu Sozeau	2014-10-02
*	Simplify evarconv thanks to new delta status of projections,	Matthieu Sozeau	2014-09-30
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Make the retroknowledge marshalable.	Arnaud Spiwack	2014-09-24
*	Clean a bit of univ.ml, add credits.	Matthieu Sozeau	2014-09-18
*	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin	2014-09-13
*	Fix generation of inductive elimination principle for primitive records.	Matthieu Sozeau	2014-09-10
*	Fix checker to handle projections with eta and universe polymorphism correctly.	Matthieu Sozeau	2014-09-06
*	Fix checker treatment of inductives using subst_instances instead of subst_un...	Matthieu Sozeau	2014-09-05
*	Rename eta_expand_ind_stacks, fix the one from the checker and adapt	Matthieu Sozeau	2014-09-05
*	Fix primitive projections declarations for inductive records.	Matthieu Sozeau	2014-09-05
*	Fix bug #3559, ensuring a canonical order of universe level quantifications when	Matthieu Sozeau	2014-09-04
*	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack	2014-09-04
*	Coqide prints succesive hyps of the same type on 1 line	Pierre Boutillier	2014-09-01
*	Simplify even further the declaration of primitive projections,	Matthieu Sozeau	2014-08-30
*	Add test-suite file. Compute the name for the record binder in the	Matthieu Sozeau	2014-08-29
*	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau	2014-08-28
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was larger...	Matthieu Sozeau	2014-08-18
*	Restrict eta-conversion to inductive records, fixing bug #3310.	Matthieu Sozeau	2014-08-14
*	Small optimization in Cooking: do not construct identity substitutions.	Pierre-Marie Pédrot	2014-08-13