coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	trying f	courtieu	2008-03-13
*	tactique Gappa : mise en place	filliatr	2008-03-11
*	Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)	herbelin	2008-03-10
*	Fix compilation problem and finish little cleanup.	msozeau	2008-03-10
*	Fix a few bugs in Program: use user-given typing constraints for	msozeau	2008-03-09
*	correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)	jforest	2008-03-08
*	f_equal, revert, specialize in ML, contradict in better Ltac (+doc)	letouzey	2008-03-07
*	Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part	msozeau	2008-03-07
*	Plug the new setoid implemtation in, leaving the original one commented	msozeau	2008-03-06
*	Syntax changes in typeclasses, remove "?" for usual implicit arguments	msozeau	2008-03-06
*	Attempt of fix for extraction of modules types	letouzey	2008-03-05
*	Rework on rich forms of rewrite	letouzey	2008-03-01
*	dead code	letouzey	2008-02-27
*	typo	letouzey	2008-02-27
*	Proper implicit arguments handling for assumptions	msozeau	2008-02-26
*	Forgotten file in previous commit	lmamane	2008-02-25
*	Merge with lmamane's private branch:	lmamane	2008-02-22
*	congruence now knows about _ -> _	corbinea	2008-02-21
*	Petite correction suite à la révision 10571	notin	2008-02-18
*	Backport Program Instance into Instance. Proper early error message if	msozeau	2008-02-10
*	Solde de code mort et petites optimisations sur lesquels je suis	herbelin	2008-02-09
*	Change implementation of resolution for typeclasses to use a customized	msozeau	2008-02-08
*	New "Preterm [ of id ] " command to show the preterm before giving it to	msozeau	2008-02-08
*	Backport code from command.ml to subtac_command.ml for definining	msozeau	2008-02-08
*	New algorithm to resolve morphisms, after discussion with Nicolas	msozeau	2008-02-06
*	Beaoucoup de changements dans la representation interne des modules.	soubiran	2008-02-01
*	Unification de TacLetRecIn et TacLetIn. En particulier, on peut	herbelin	2008-02-01
*	Fix obvious syntax error. Forgot to recompile before commiting...	msozeau	2008-01-31
*	Finish let\| implementation and document it	msozeau	2008-01-31
*	Work on dependent induction tactic and friends, finish the test-suite example	msozeau	2008-01-30
*	Use new redefinition support for the default obligations tactic	msozeau	2008-01-30
*	Correction du bug #1785	notin	2008-01-29
*	Récupération d'une exception Not_found	notin	2008-01-22
*	cosmetics: after an extract inductive to bool, let's use if then else	letouzey	2008-01-20
*	Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...	msozeau	2008-01-18
*	Change notation for setoid inequality, coerce objects before comparing them. ...	msozeau	2008-01-18
*	Add new LetPattern construct to replace dest. syntax: let\| pat := t in b is b...	msozeau	2008-01-17
*	Generalize instance declarations to any context, better name handling. Add ho...	msozeau	2008-01-15
*	Correction of bug #1769	jforest	2008-01-09
*	Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...	msozeau	2008-01-07
*	Completion of 10427...	herbelin	2008-01-07
*	Add partial setoids in theories/Classes, add SetoidDec class for setoids with...	msozeau	2008-01-04
*	Fix name capture bug and call the right pretyper in subtac.	msozeau	2007-12-31
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Suppression de commentaires inutiles	notin	2007-12-19
*	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack	2007-12-06
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	bug correction in functional inversion principle generation	jforest	2007-11-27
*	minor bug correction in Function	jforest	2007-11-26
*	Extraction inlines Wf.Fix by default (wish of Y.Bertot)	letouzey	2007-11-21