coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	_tags: lexer.ml4 now uses pa_macro	letouzey	2009-04-28
*	Backporting 12112 from v8.2 branch to trunk (fixing documentation bugs	herbelin	2009-04-28
*	Cleanup old eauto code.	msozeau	2009-04-27
*	- Implementation of a new typeclasses eauto procedure based on success	msozeau	2009-04-27
*	- Fixed a little bug in previous commit (bad failure in case of unknown entry).	herbelin	2009-04-27
*	- Cleaning (unification of ML names, removal of obsolete code,	herbelin	2009-04-27
*	- Fixing #2090 (occur check missing when trying to solve evar-evar equation).	herbelin	2009-04-25