coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix bug #2473 due to wrong folding of the evar environment	msozeau	2011-10-18
*	Fix bug #2227	msozeau	2011-10-18
*	Fix inductive coercion code in Program (bug #2378)	msozeau	2011-10-18
*	Fix bug #2586 and enhance clsubst* as well as a side effect	msozeau	2011-10-18
*	Revert "New evar_map printer ppevmfull which can typically be installed for"	herbelin	2011-10-17
*	Partly reverting r14539 about fully expanding "let-in"s and not just	herbelin	2011-10-17
*	New evar_map printer ppevmfull which can typically be installed for	herbelin	2011-10-17
*	Patch by Dan Grayson to ensure that "Add LoadPath ... as ..." closes	herbelin	2011-10-17
*	Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...	msozeau	2011-10-17
*	dev/base_include: display a nice message at the end of the load	letouzey	2011-10-15
*	debugging.txt: no more typing of #use "include" if using .ocamlinit	letouzey	2011-10-15
*	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