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