coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Mod_subt: some more refactoring, substitution is also separated in two tables	letouzey	2011-02-11
*	Mod_subst: split delta_resolver in two tables (mp / kn)	letouzey	2011-02-11
*	Update changelogs	glondu	2011-02-11
*	In evars_of_term and co, visit array c in Evar(_,c) (sequel to r13809)	letouzey	2011-02-11
*	Try to clarify a bit Class_tactics (comments, refactoring,...)	letouzey	2011-02-11
*	An generic imperative union-find, used for deps of evars in Class_tactics	letouzey	2011-02-11
*	Change Evd.fold to a faster version that simply removes unneeded evars.	msozeau	2011-02-11
*	compatibility <3.12 (Map.exists Map.singleton)	pboutill	2011-02-11
*	Remove obsolete TheoryList	glondu	2011-02-10
*	Vectors fully use implicit arguments	pboutill	2011-02-10
*	Fixpoints are traverse during implicits arguments search to toplevel	pboutill	2011-02-10
*	Interp a definition with the implicit arguments of its local context	pboutill	2011-02-10
*	local variables can have implicits locally	pboutill	2011-02-10
*	Data structure telling implicits of local variables is a map in the	pboutill	2011-02-10
*	internalize now use a record for its env	pboutill	2011-02-10
*	MacOS compatibility	pboutill	2011-02-10
*	More comments and less doublons in some mli	pboutill	2011-02-10
*	- proper printing of setoid_rewrite tactic applications	msozeau	2011-02-10
*	Rename subst_raw_with_bindings to subst_glob_with_bindings and export	msozeau	2011-02-10
*	Started to fix the declarative proof mode (C-zar).	aspiwack	2011-02-10
*	One more fix for setoid_rewrite: completely reinterpret the given lemmas	msozeau	2011-02-09
*	Correct handling of existential variables when multiple different	msozeau	2011-02-08
*	Factorize code of rewrite to make way for a new implementation using the	msozeau	2011-02-07
*	Dp: another fix suggested by Virgile Prevosto	letouzey	2011-02-03
*	Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)	letouzey	2011-02-03
*	Coqlib.gen_constant_in_modules can take a qualid string "Foo.bar"	letouzey	2011-01-31
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	test-suite/Makefile: add a rule to build all_stdlib.v (for the bench)	glondu	2011-01-27
*	Make simpl use the proper constant when folding (mutual) fixpoints	letouzey	2011-01-27
*	Fix compilation with camlp5 (Closes: #2487)	glondu	2011-01-25
*	Update .gitignore	glondu	2011-01-25
*	Add a test for sorting all universes of stdlib	glondu	2011-01-25
*	Rewrite sort_universes to minimize the number of universes	glondu	2011-01-25
*	Numbers: simplier spec for testbit	letouzey	2011-01-20
*	Fix formatting issue in refman	glondu	2011-01-12
*	Fix ocamlbuild-based build system	glondu	2011-01-11
*	Remove references to -ide option of coqmktop	glondu	2011-01-11
*	In univ.ml, put universe_level primitives in its their own sub-module	glondu	2011-01-11
*	Add [Typeclasses Debug] option that respects backtracking, solve	msozeau	2011-01-11
*	Add "Print Sorted Universes"	glondu	2011-01-11
*	Use dashed lines for equivalence edges in dot output of universes	glondu	2011-01-11
*	More coherent comment ordering	glondu	2011-01-11
*	Fix some typos	glondu	2011-01-11
*	ratrapage exception, deja fait ...	bgregoir	2011-01-11
*	Fixing an uncaught exception bug with use of vmcast	herbelin	2011-01-07
*	MacOS integration	pboutill	2011-01-07
*	Separate load_file handler in coqide	pboutill	2011-01-07
*	Coqide is not built with coqmktop any more	pboutill	2011-01-07
*	Don't install both coqide.byte and coqide.opt	pboutill	2011-01-07