coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	closed bug 1898: fold x in x; added a reordering primitive tactic	barras	2008-11-26
*	correction bug 1997.	soubiran	2008-11-25
*	eventually fixing r11612	barras	2008-11-24
*	amelioration mineur du comportement de Function	jforest	2008-11-24
*	first attempt to allow Function to deal with dependent pattern matching. This...	jforest	2008-11-23
*	- Synchronized subst_object with load_object (load_and_subst_objects)	herbelin	2008-11-23
*	Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b	herbelin	2008-11-23
*	Minor improvement to commit 11619	herbelin	2008-11-23
*	Fixed bug #2006 (type constraint on Record was not taken into account) +	herbelin	2008-11-23
*	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin	2008-11-22
*	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin	2008-11-22
*	fixed problem with r11612	barras	2008-11-21
*	fixed exponential behavior of evar unif (ground case)	barras	2008-11-21
*	correction of bug #2002	jforest	2008-11-20
*	Add implicit rules for native plugins (.cmxs)	glondu	2008-11-19
*	Execute #rectypes directive in embedded OCaml toplevel...	glondu	2008-11-19
*	Fix typo in omega doc	glondu	2008-11-19
*	integrate suggestions by B. Baydemir (see #1930)	letouzey	2008-11-17
*	Univ: two < instead of a Pervasives.compare on int (as suggested by X. Leroy)	letouzey	2008-11-16
*	Correct display of constraints for Print Universes "dumpfile"	letouzey	2008-11-15
*	Amélioration du README.doc et de l'installation de la doc	notin	2008-11-14
*	Restores behaviour of v8.1 for unification problems which fail (backport of 1...	letouzey	2008-11-14
*	Faster comparison of universes	letouzey	2008-11-14
*	make doc ne compilait plus la doc de stdlib (bug #1996)	notin	2008-11-14
*	Add missing test-suite files for closed bugs.	msozeau	2008-11-14
*	retour sur le commit 11579 qui faisait plante les contribs FSet et color.	soubiran	2008-11-14
*	Tentative d'amélioration de la robustesse des Makefile générés par	notin	2008-11-13
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11583 85f007b7-540e-0...	barras	2008-11-13
*	Correction du bug #1995	notin	2008-11-12
*	Les signatures des applications de foncteur sont précalculées, cela alourdi...	soubiran	2008-11-12
*	Makefile.build: an OPTFLAGS behind a bytecode ocamlc (which refuses -p)	letouzey	2008-11-10
*	Fix mixup between Record, Structure and Class by adding a new variant for	msozeau	2008-11-10
*	Fix bug reported by Mark Dickinson on Coq-Club about [setoid_rewrite] not	msozeau	2008-11-10
*	- Correction erreur dans test output Notation.v	herbelin	2008-11-09
*	f_equal : solve an inefficiency issue (apply vs. simple apply)	letouzey	2008-11-09
*	better fix for #1931 by using sort_of	letouzey	2008-11-09
*	Oops... forgot to commit a file related to r11561.	msozeau	2008-11-09
*	Add test-suite file related to discussion of syntax of implicit binders.	msozeau	2008-11-09
*	More factorization of inductive/record and typeclasses: move class	msozeau	2008-11-09
*	- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in	herbelin	2008-11-09
*	Apply vmconv if there are no _undefined_ evars around.	msozeau	2008-11-08
*	Slight change of the semantics of user-given casts: they don't really	msozeau	2008-11-07
*	- Ajout possibilité de lancer ocamldebug sur coqide	herbelin	2008-11-07
*	Suite #11533	notin	2008-11-07
*	Correction du bug #1926	notin	2008-11-07
*	Add some example uses of the new record features in Record.v:	msozeau	2008-11-07
*	Fix a bug in the specialization by unification tactic related to the problems	msozeau	2008-11-07
*	Add the ability to give a specific tactic to solve each obligation in	msozeau	2008-11-07
*	Fix universe problem appearing ConCaT using the existing infrastructure for	msozeau	2008-11-07
*	Cosmetic: no more whitespace at end of lines in extraction files	letouzey	2008-11-06