coq - The formal proof system

Age	Commit message (Expand)	Author
2009-06-09	Correct handling of the initial existentials from the goal and the ones	msozeau
2009-06-08	Do a fixpoint on the result of typeclass search to force the	msozeau
2009-06-08	Change in UI behaviour : proof folding is now done by double clicking. Delay is	vgross
2009-06-07	File forgotten in commit 12171.	herbelin
2009-06-07	Partial simplification of undo mechanism, relying only on Courtieu's	herbelin
2009-06-07	- Added two new introduction patterns with the following temptative syntaxes:	herbelin
2009-06-06	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-03	Ensure the precondition of the partial function [list_chop] holds	msozeau
2009-06-02	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-01	## 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-05-29	Fix extract hyps to correctly discharge all hyps as described by keep	msozeau
2009-05-28	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-27	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-26	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-24	Temporary fixes in unification:	msozeau
2009-05-24	Moved and completed the history of Coq versions from the	herbelin
2009-05-23	A try at using sort variables during unification. Instead of refreshing	msozeau
2009-05-20	Many fixes in unification:	msozeau
2009-05-20	- Fixing declarative mode in presence of high use of Change_evars nodes	herbelin
2009-05-19	Fix in canonical structure resolution: [check_conv_record] may return	msozeau
2009-05-19	Remove camlp4-specific exception handling	msozeau
2009-05-18	Minor unification changes:	msozeau
2009-05-17	- Allowing multiple calls to tactic fix with automatic generation of	herbelin
2009-05-16	(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-13	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-11	micromega: proof compression bugfix	fbesson
2009-05-10	- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it	herbelin
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin