coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	modifs de nsatz suggerees par Hugo	pottier	2010-06-25
*	Restored a "feature" of unification in pre-8.3 (it was used e.g. in a	herbelin	2010-06-25
*	Extraction: nicer simple extraction of custom defs (fix #2204)	letouzey	2010-06-23
*	Names: remove obsolete mod_self_id	letouzey	2010-06-23
*	Ajout d'une feuille de style pour les définitions spécifiques à Hevea + di...	notin	2010-06-23
*	Mise à jour des liens au site Coq (suite à la MAJ de la redirection DNS de ...	notin	2010-06-23
*	Commit 13179 continued (updated CHANGES about support for Heq's library).	herbelin	2010-06-22
*	Backport from trunk to 8.3 of modifications on groebner/nsatz	herbelin	2010-06-22
*	Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).	herbelin	2010-06-22
*	Fixing dependencies for coqide	vgross	2010-06-22
*	fix bug #2318, parsing error on dos line endings	vgross	2010-06-22
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Protection against anomaly when loading a state with bad magic number.	herbelin	2010-06-22
*	Extraction: replace unicode characters in ident by ascii encodings (fix #2158...	letouzey	2010-06-21
*	Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)	letouzey	2010-06-20
*	clear/revert dependent: restrict to hyp(h) instead of ident(h)	letouzey	2010-06-18
*	Quick fix for having clenv debug printer working in trunk.	herbelin	2010-06-18
*	Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).	herbelin	2010-06-18
*	Documentation of clear dependent and revert dependent	letouzey	2010-06-18
*	add in test-suite the scripts about fsetdec bugs	letouzey	2010-06-18
*	Report fixes from FSetDecide to MSetDecide	letouzey	2010-06-18
*	fsetdec: a forgotten Set instead of Type was breaking discard_nonFset (fix #2...	letouzey	2010-06-18
*	fsetdec: clear dependent hypothesis before anything else (fix #2136).	letouzey	2010-06-17
*	New tactic "clear dependent", for the moment in ltac in Init/Tactics	letouzey	2010-06-17
*	test for bug #2141 (include + extraction)	letouzey	2010-06-16
*	MSetInterface: no induction principle about a Record (nicer extraction)	letouzey	2010-06-16
*	Extraction: fix the eta reduction function used in code optimisations	letouzey	2010-06-16
*	MSetAVL: for nicer extraction, we create only tree_ind, not tree_rect and tre...	letouzey	2010-06-15
*	CHANGE: a word about new commands Compute and Fail	letouzey	2010-06-15
*	CHANGES: list of modifications for the extraction	letouzey	2010-06-15
*	Extraction: in support library, more and nicer big_int	letouzey	2010-06-15
*	Update of Extraction documentation	letouzey	2010-06-14
*	Fixed commit 13125 (stricter check of induction args): an interpretation	herbelin	2010-06-14
*	Alert on the possible incompatibilties with set_add (see bug 2111) which	herbelin	2010-06-14
*	Extraction Implicit: documentation	letouzey	2010-06-14
*	Added printing of recursive notations in cases pattern (supported by wish 2248).	herbelin	2010-06-14
*	Fixing bug 2295 (omission of option "as" in return clause of "match" was not	herbelin	2010-06-13
*	Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).	herbelin	2010-06-13
*	Addressed bug #2320 in v8.2 and v8.3 branches ("refine" problem with	herbelin	2010-06-13
*	Fixing definition of set_map (bug report #2111) which was actually already	herbelin	2010-06-13
*	Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"	herbelin	2010-06-13
*	Fixed bug #2314 (inversion using not checking the correctness of its arguments	herbelin	2010-06-13
*	Made intros_until and onInductionArg a bit stricter and robust	herbelin	2010-06-13
*	Fixed a bug in pretty-printing "induction" and "destruct" due to a	herbelin	2010-06-13
*	Fixed bug #2135 (second-order unification was raising cryptic message)	herbelin	2010-06-12
*	Added regression tests for bugs + miscellaneous improvements	herbelin	2010-06-12
*	Applying François' patch fixing grammar of uniform inheritance condition mes...	herbelin	2010-06-12
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Improved the inference of the return predicate in dependent pattern-matching.	herbelin	2010-06-12
*	Added rudimentary support for using constructors from the explicit	herbelin	2010-06-12