coq - The formal proof system

Age	Commit message (Expand)	Author
2008-11-26	closed bug 1898: fold x in x; added a reordering primitive tactic	barras
2008-11-26	closed bug 1898: fold x in x; added a reordering primitive tactic	barras
2008-11-25	correction bug 1997.	soubiran
2008-11-24	eventually fixing r11612	barras
2008-11-24	amelioration mineur du comportement de Function	jforest
2008-11-23	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-22	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-21	fixed problem with r11612	barras
2008-11-21	fixed exponential behavior of evar unif (ground case)	barras
2008-11-20	correction of bug #2002	jforest
2008-11-19	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-17	integrate suggestions by B. Baydemir (see #1930)	letouzey
2008-11-16	Univ: two < instead of a Pervasives.compare on int (as suggested by X. Leroy)	letouzey
2008-11-15	Correct display of constraints for Print Universes "dumpfile"	letouzey
2008-11-14	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-13	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-12	Correction du bug #1995	notin
2008-11-12	Les signatures des applications de foncteur sont précalculées, cela alourdi...	soubiran
2008-11-10	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-09	- 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-08	Apply vmconv if there are no _undefined_ evars around.	msozeau
2008-11-07	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