coq - The formal proof system

Age	Commit message (Expand)	Author
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-17	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-15	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-14	MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_right	letouzey
2011-10-12	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-11	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-10	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-09	mainbiblio.bib : get rid of merge marker from failed merge	letouzey
2011-10-08	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-07	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-05	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