coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Makefile made compatible with Solaris 10 (bug #2078, continued - see	herbelin	2009-06-06
*	Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0	herbelin	2009-06-06
*	Fixing bug #2106 ("match" compilation with multi-dependent constructor).	herbelin	2009-06-06
*	Very-small-step policy changes to the library.	herbelin	2009-06-06
*	Applying Ian Lynagh's documentation fixes patch (see bug #2112)	herbelin	2009-06-06
*	Ensure the precondition of the partial function [list_chop] holds	msozeau	2009-06-03
*	Adding a regression test about Bauer's example on coq-club of	herbelin	2009-06-02
*	Use Type instead of Set.	msozeau	2009-06-02
*	Backtrack on experimental unification with sort variables: it requires	msozeau	2009-06-02
*	Fix script file using the "Manual Implicit" flag.	msozeau	2009-06-02
*	## Lines starting with '## ' will be removed from the log message.	msozeau	2009-06-01
*	Change unification with sort constraints to not use the kernel	msozeau	2009-06-01
*	Prevent automatic inference of implicit arguments when the auto flag is	msozeau	2009-06-01
*	Fix extract hyps to correctly discharge all hyps as described by keep	msozeau	2009-05-29
*	Properly catch sort constraint inconsistency exception in	msozeau	2009-05-28
*	Adapted the emacs mode to font-lock. Re-using code from ProofGeneral.	courtieu	2009-05-28
*	Ajout d'un printer modulaire pour les constr. C'est-à-dire une fonction	aspiwack	2009-05-28
*	Fix implicit args code so that declarations are added for all	msozeau	2009-05-27
*	Populate the sort constraints set correctly during unification. Add a	msozeau	2009-05-27
*	Stop using a "Manual Implicit Arguments" flag and support them as soon	msozeau	2009-05-27
*	Ajout d'une fonction Lexer.remove_keyword pour libérer un keyword dans	aspiwack	2009-05-27
*	=?utf-8?q?D=C3=A9sinterdiction=20de=20GDELETE=5FRULE=20dans=20pcoq.ml4.=20Mal...	aspiwack	2009-05-27
*	sane behaviour for copy/paste operations (the code is still insane, though)	vgross	2009-05-27
*	keeping interface synch'ed	vgross	2009-05-27
*	dead code pruning	vgross	2009-05-27
*	Fix de Bruijn lifting bug appearing when we match on multiple terms with	msozeau	2009-05-26
*	ocamldebug-coq: add some forgotten -I	letouzey	2009-05-26
*	Temporary fixes in unification:	msozeau	2009-05-24
*	Moved and completed the history of Coq versions from the	herbelin	2009-05-24
*	A try at using sort variables during unification. Instead of refreshing	msozeau	2009-05-23
*	Many fixes in unification:	msozeau	2009-05-20
*	- Fixing declarative mode in presence of high use of Change_evars nodes	herbelin	2009-05-20
*	Fix in canonical structure resolution: [check_conv_record] may return	msozeau	2009-05-19
*	Remove camlp4-specific exception handling	msozeau	2009-05-19
*	Minor unification changes:	msozeau	2009-05-18
*	- Allowing multiple calls to tactic fix with automatic generation of	herbelin	2009-05-17
*	(Tentative to) add Canonical Structure resolution to the regular	msozeau	2009-05-16
*	Minor fixes in typeclasses:	msozeau	2009-05-16
*	Support for definition hooks in subtac.	msozeau	2009-05-16
*	Fix to my last notation patch: now fixpoint are correctly handled	vsiles	2009-05-13
*	minor bugfixes. CoqIde development will resume soon now ...	vgross	2009-05-13
*	micromega: proof compression bugfix	fbesson	2009-05-11
*	- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it	herbelin	2009-05-10
*	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin	2009-05-09
*	fix a bug in canonical structures (bug found and fixed by Cyril)	barras	2009-05-09
*	adds a theorem to reason at the level of Z	bertot	2009-05-07
*	Improvements in typeclasses eauto and generalized rewriting:	msozeau	2009-05-05
*	Fix a small notation/scope bug:	vsiles	2009-04-30
*	More efficient handling of evars in Program Fixpoint commands.	msozeau	2009-04-28
*	Fixes for bugs in r12110:	msozeau	2009-04-28