coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_right	letouzey	2011-10-14
*	Temporary revert commit 14550 since it breaks a few contribs	letouzey	2011-10-12
*	Patch to support (a priori) all versions of make 3.xx >= 3.81	herbelin	2011-10-12
*	test-suite: non-regression test for bug #2603	letouzey	2011-10-12
*	Added test for bug #2615	herbelin	2011-10-11
*	Safe_typing: adding a inductive block adds many labels (fix #2603)	letouzey	2011-10-11
*	Names : check of labels, cleanup, nicer debug display of kn and constant	letouzey	2011-10-11
*	Mod_subst: an unused function	letouzey	2011-10-11
*	in heads.ml, at least turn the Not_found of #2608 into assert false	letouzey	2011-10-11
*	Completing r14538 (Chung-Kil Hur's trick for fast dependently-typed	herbelin	2011-10-11
*	Unification in the return clause of match was not supported in solve_evars.	herbelin	2011-10-11
*	Moved to a more standard order of arguments (i.e. env followed by evar_map)	herbelin	2011-10-11
*	More on r14536 (an unused pattern-matching remained in the commit).	herbelin	2011-10-11
*	Various simplifications about constant_of_delta and mind_of_delta	letouzey	2011-10-11
*	Hash-consing of mutual_inductive_body (and Univ.constraints)	letouzey	2011-10-10
*	Avoid some re-allocation during hash-cons of dir_path	letouzey	2011-10-10
*	Hash-cons the statically allocated Rels (1 to 16) to themselves	letouzey	2011-10-10
*	Hashtbl_alt : typo in a comment	letouzey	2011-10-10
*	Hash-cons of constr : avoid some useless allocations	letouzey	2011-10-10
*	More robust and uniform treatment of aliases in evarutil.ml	herbelin	2011-10-10
*	Applied the trick of Chung-Kil Hur to solve second-order matching	herbelin	2011-10-10
*	Fixing buggy abberant code for Evarutil.expand_evar	herbelin	2011-10-10
*	Little code simplification of instantiate_evar in evd.ml	herbelin	2011-10-10
*	Added information about evar origin in pretty-printing evd for debug	herbelin	2011-10-10
*	Passed conv_algo to evar_define and move call to solve_refl to	herbelin	2011-10-10
*	Proper fix for complement/flip instances.	msozeau	2011-10-10
*	mainbiblio.bib : get rid of merge marker from failed merge	letouzey	2011-10-09
*	Scheme names: Use unprobable names + ensure names do not hide existing names	herbelin	2011-10-08
*	Rely on kernel to know if a name is already used so as to be consistent with it.	herbelin	2011-10-08
*	fsetdec : non-atomic elements are now transformed as variables first (fix #2464)	letouzey	2011-10-07
*	A new tactic is_var to check whether a term is a goal/section variable	letouzey	2011-10-07
*	Fix bug #2557 and an issue with Propers for complement	msozeau	2011-10-07
*	Remove 'status' of Program and explain the :> better, as well as referencing ...	msozeau	2011-10-07
*	Improved handling of element equalities in fsetdec (fix #2467)	letouzey	2011-10-07
*	ocamlbuild: remove -dllpath from coqrunbyteflags	glondu	2011-10-07
*	ocamlbuild: Fix ocamlbuild compilation for changes to configure from r14500.	glondu	2011-10-07
*	Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).	herbelin	2011-10-05
*	When a pattern match, don't use the first matching term but an	herbelin	2011-10-05
*	Removing vernacular code mistakenly committed.	herbelin	2011-10-05
*	Fixing critical inductive polymorphism bug found by Bruno.	herbelin	2011-10-05
*	Force dependency of Reference-Manual.pdf over Reference-Manual.dvi	herbelin	2011-10-05
*	Use an ad-hoc monomorphic list in RelationClasses to avoid some universe cons...	letouzey	2011-10-05
*	It happens that the type inference algorithm (pretyping) did not check	herbelin	2011-10-05
*	Hash-consing of constr could share more	letouzey	2011-10-02
*	Updating some links in the FAQ	herbelin	2011-10-01
*	Moving never-used comments from Zhints.v to dev/doc so as not to	herbelin	2011-10-01
*	Fixing critical part of bug #2504. Not all inductive types in Type are	herbelin	2011-10-01
*	In Coq_config: get rid of coqsrc and make coqlib optional	glondu	2011-09-27
*	Added support for referring to subterms of the goal by pattern.	herbelin	2011-09-26
*	Generalizing subst_term_occ so that it supports an arbitrary matching	herbelin	2011-09-26