coq - The formal proof system

Age	Commit message (Expand)	Author
2010-07-22	Switch to American spelling for "internalise" and "internalisation"	herbelin
2010-07-22	Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).	herbelin
2010-07-22	Made coercions active only when modules are imported.	herbelin
2010-07-22	Backported r13308 (ConstructiveEpsilon.v) to branch v8.3	herbelin
2010-07-22	Update of ConstructiveEpsilon.v by Jean-François Monin.	herbelin
2010-07-22	Adding the destauto tactic, that reduces match by destructing matched	courtieu
2010-07-22	ported bug fix r13290 to checker	barras
2010-07-21	Fix for bug #2350 was really too quick. Here is a version that works better.	herbelin
2010-07-21	Backporting fix to bug #2353 (fixpoint with recursively non-uniform	herbelin
2010-07-21	Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).	herbelin
2010-07-21	Applied Pierre Letouzey's patch restoring Convert_concl VM casts in new proof	herbelin
2010-07-20	Fixed a bug in list_forall2eq (wrong exception was caught).	herbelin
2010-07-18	Fixed parsing of "Generalizable Variable A" ("Variable" turns to be a keyword).	herbelin
2010-07-18	Reverted 13293 commited mistakenly. Sorry for the noise.	herbelin
2010-07-18	Tentative de suppression de l'import automatique des hints et coercions.	herbelin
2010-07-16	Amelioration dans Function	jforest
2010-07-16	fixed (serious) bug #2353: non-recursive parameters of nested inductive types...	barras
2010-07-16	removed a potentially dangerous try ... with _ -> ...	barras
2010-07-16	MSetPositive: mention MSetInterface instead of FSetInterface	letouzey
2010-07-16	FSetPositive: sets of positive inspired by FMapPositive.	letouzey
2010-07-16	Bool: shorter and more systematic proofs + an iff lemma about eqb	letouzey
2010-07-16	fixed bug #2316 (ring_simplify)	barras
2010-07-15	Be more clever when trying to find out the relation in	msozeau
2010-07-15	Extraction: fix a bit the extraction under modules	letouzey
2010-07-15	Ocamlbuild: adapt to last changes for camlp4 (use of tools/compat5*.cmo)	letouzey
2010-07-12	Fix compilation and test-suite of nsatz	glondu
2010-07-12	coqide: s/Sys.argv.(0)/Sys.executable_name/ for coqtop (cf #2341)	glondu
2010-07-10	Bool: iff lemmas about or, a reflect inductive, an is_true function	letouzey
2010-07-09	Finish adding out-of-the-box support for camlp4	letouzey
2010-07-08	Extraction: restrict autoinling to csts whose body is globally visible (fix #...	letouzey
2010-07-08	Updating reference manual credits: gb is now nsatz.	herbelin
2010-07-08	Extraction: more factorization of common match branches	letouzey
2010-07-08	Extraction: Unset Extraction AutoInline is now the default	letouzey
2010-07-08	nsatz in an integral domain with specialization to Z and R	pottier
2010-07-07	Fixed compilation with statically-linked plugins (the decl_mode	herbelin
2010-07-07	Extraction Library Foo creates Foo.ml, not foo.ml (correct version)	letouzey
2010-07-07	Extraction Library Foo creates Foo.ml, not foo.ml	letouzey
2010-07-07	CHANGES: mention last-minute improvements of extraction	letouzey
2010-07-07	Extraction: get advantage of nicer, algebraic, module types	letouzey
2010-07-07	Extraction: some more work on the (re)naming framework	letouzey
2010-07-07	Mod_typing: fix the content of the typ_expr_alg field	letouzey
2010-07-05	Fix goal display when backtracking	vgross
2010-07-05	Robustness fix : clean restart of coqtop on pipe error + force matching	vgross
2010-07-05	Turned off Mac dynlink hack for 10.6.3+ on x86_64	thutchin
2010-07-05	Stronger checks on coqtop termination, warning when zombies.	vgross
2010-07-05	Extraction: (yet another) rework of the renaming code	letouzey
2010-07-05	FSets/Msets: some renaming of module params to simplify the task of the extra...	letouzey
2010-07-02	Fixing tabs closing problems by removing activation infrastructure.	vgross
2010-07-02	Extraction: better support of modules	letouzey
2010-07-02	Extraction: no more MPself hence no need for subst during pp	letouzey