coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Various fixes on typeclasses:	msozeau	2008-03-27
*	Fix a bug found by B. Grégoire when declaring morphisms in module	msozeau	2008-03-23
*	Une passe sur les réels:	herbelin	2008-03-23
*	Do another pass on the typeclasses code. Correct globalization of class	msozeau	2008-03-19
*	tactique gappa	filliatr	2008-03-19
*	Added a function to rebuild an elim scheme from elim_scheme_info. Will	courtieu	2008-03-18
*	Removed unneeded tactics from RelationClasses. Use	msozeau	2008-03-16
*	Reorganize Program and Classes theories. Requiring Setoid no longer sets	msozeau	2008-03-16
*	Minor fixes on setoid rewriting. Now uses definitions of [relation] and	msozeau	2008-03-16
*	Do a second pass on the treatment of user-given implicit arguments. Now	msozeau	2008-03-15
*	Adapt funind to the RLetPattern constructor.	msozeau	2008-03-15
*	avoid universe problems with pf_get_type in f_equal	letouzey	2008-03-14
*	Backtrack wrong commit.	courtieu	2008-03-14
*	kill a warning (and clean the code around)	letouzey	2008-03-14
*	nettoyage de code obsolete.	soubiran	2008-03-14
*	Ajout des alias de module dans le noyau.	soubiran	2008-03-14
*	tactique gappa	filliatr	2008-03-14
*	indentation.	courtieu	2008-03-14
*	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