coq - The formal proof system

Age	Commit message (Expand)	Author
2009-06-26	Add doc for [Print Opaque Dependencies] and a better explanation for the	msozeau
2009-06-22	Correct treatment of dependent products in signatures: create the evars	msozeau
2009-06-22	Fixes for r12197, the refined evars were not returned in case fail_evar	msozeau
2009-06-22	documented a bug of pattern unification with metas	barras
2009-06-22	made several occurrences of (eapply ...; eauto) not rely on the lack of patte...	barras
2009-06-22	Report de la révision #12200 (bug #2125)	notin
2009-06-22	remove some unused functions (which are part of a soon-to-be obsolete	vgross
2009-06-22	clearing unused functions	vgross
2009-06-18	Use more consistent resolution parameters in Program and regular typing	msozeau
2009-06-18	Fix "unsatisfiable constraints" error messages to include all the	msozeau
2009-06-18	Try typeclass resolution in coercion if no solution can be found to a	msozeau
2009-06-17	Fallback on not using [fix_proto] if the right imports aren't there, the	msozeau
2009-06-16	Reimplementation of leibniz rewrite to control the instantiation of the	msozeau
2009-06-15	Allow anonymous instances again, with syntax [Instance: T] where T	msozeau
2009-06-13	Correct typo: -noglob takes no argument.	msozeau
2009-06-11	Use a lazy value for the message in FailError, so that it won't be	msozeau
2009-06-11	Simplifying the call to print_no_goals and not calling it when no goal	herbelin
2009-06-11	When typing a non-dependent arrow, do not put the (anonymous) variable	msozeau
2009-06-10	Accept more Unicode symbols	glondu
2009-06-10	Use the projections for reflexivity, symmetry and transitivity proofs to	msozeau
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