| Age | Commit message (Expand) | Author |
|---|
| 2009-03-20 | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ... | letouzey |
| 2009-03-14 | Makefile: ml dependencies of contribs are moved to .mllib files | letouzey |
| 2008-12-31 | Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod -> | herbelin |
| 2008-12-09 | About "apply in": | herbelin |
| 2008-11-09 | f_equal : solve an inefficiency issue (apply vs. simple apply) | letouzey |
| 2008-11-09 | better fix for #1931 by using sort_of | letouzey |
| 2008-09-14 | Fix bug #1931 by searching for a sort after doing beta,iota,delta- | msozeau |
| 2008-03-14 | avoid universe problems with pf_get_type in f_equal | letouzey |
| 2008-03-07 | f_equal, revert, specialize in ML, contradict in better Ltac (+doc) | letouzey |
| 2008-02-21 | congruence now knows about _ -> _ | corbinea |
| 2007-10-18 | added generation from trivial patterns for congruence | corbinea |
| 2007-10-16 | Fixed congruence instance generator + changed default depth to 1000 | corbinea |
| 2007-09-14 | Correction du bug #1679 (congruence) et ajout test-suite | corbinea |
| 2007-07-24 | Declarative language: fixed the generation of fixpoints for induction proofs. | corbinea |
| 2007-05-24 | fixed (PR#1483) | corbinea |
| 2007-03-15 | Suppression argument pattern_source du case_info (code jamais utilisé) | herbelin |
| 2006-09-19 | added congruence improvement | corbinea |
| 2006-04-28 | Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '... | notin |
| 2006-01-21 | Messages de idtac et fail peuvent maintenant être des listes de string, int ... | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme... | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-11-02 | Types inductifs parametriques | mohring |
| 2005-08-17 | new congruence | corbinea |
| 2005-02-18 | Standardisation of function names about global references (especially, renami... | herbelin |
| 2005-02-12 | Uniformisation de destApplication en destApp | herbelin |
| 2005-02-06 | Nettoyage et documentation de Library | herbelin |
| 2005-01-14 | Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed | sacerdot |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-03-15 | oops | corbinea |
| 2004-03-14 | minor changes | corbinea |
| 2004-03-14 | congruence now handles disequalities | corbinea |
| 2004-02-06 | correction de bugs de congruence et firstorder (inductifs) | corbinea |
| 2004-01-09 | bugs avec Pose et Assert | barras |
| 2003-12-09 | cc update | corbinea |
| 2003-12-02 | error messages adjustement | corbinea |
| 2003-11-29 | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin |
| 2003-11-29 | ground->firstorder, cc-> congruence, CC final commit | corbinea |
| 2003-11-26 | just forgot something in previous commit | corbinea |
| 2003-11-26 | removal of CC.v lemata in cc (deprecated) | corbinea |
| 2003-11-25 | CC: added injection theory | corbinea |
| 2003-11-20 | Code simplification in CC | corbinea |
| 2003-10-03 | Cacher les .v8 | herbelin |
| 2003-05-25 | Ground and CCsolve updates | corbinea |
| 2003-03-31 | factorisation des "constant" dans les contrib/* ( maintenant dans coqlib ) | corbinea |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-10-01 | Adding the congruence closure tactics (CC and CCsolve). | corbinea |
