| Age | Commit message (Expand) | Author |
|---|
| 2008-03-23 | Nettoyage Wf.v et unification (suite remarques faites sur cocorico) | herbelin |
| 2008-03-23 | Une passe sur les réels: | herbelin |
| 2008-03-15 | Do a second pass on the treatment of user-given implicit arguments. Now | msozeau |
| 2008-03-07 | f_equal, revert, specialize in ML, contradict in better Ltac (+doc) | letouzey |
| 2008-03-04 | still one more substituion s/Set/Type/ | letouzey |
| 2008-02-26 | Proper implicit arguments handling for assumptions | msozeau |
| 2008-01-23 | Typo | notin |
| 2007-12-17 | Quelques arguments en plus... | glondu |
| 2007-11-08 | Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic. | emakarov |
| 2007-11-06 | small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is | letouzey |
| 2007-11-06 | Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of... | letouzey |
| 2007-11-01 | A way to specialize universally quantified hypothesis: if H is | letouzey |
| 2007-10-05 | Added the automatic generation of the boolean equality if possible and the | vsiles |
| 2007-10-03 | Révision de theories/Logic concernant les axiomes de descriptions. | herbelin |
| 2007-09-30 | Ajout infos de débogage de "universe inconsistency" quand option Set | herbelin |
| 2007-08-08 | Fix dependency bugs due to Program modules renamings. | msozeau |
| 2007-08-07 | Move Program tactics into a proper theories/ directory as they are general pu... | msozeau |
| 2007-06-22 | Ajout exist & cie à la table des hints par symétrie avec ex_intro & | herbelin |
| 2007-06-08 | Removed an extra \tacindex occurrence for the tactic discriminate. | emakarov |
| 2007-06-05 | Gestion espaces dans notation _ = _ :> _ | herbelin |
| 2007-04-28 | Déplacement des opérations sur bool dans l'état initial | herbelin |
| 2007-04-02 | Added back the tactics [apply -> ident], etc. to Tactics.v after | emakarov |
| 2007-04-01 | Removed the definition of extensions of apply to equivalences | emakarov |
| 2007-03-30 | Added new tactics for applying equivalences (iff) to Tactics.v: | emakarov |
| 2007-03-26 | stupid me: ?f two times in a pattern | letouzey |
| 2007-01-02 | Add f_equal case for 6 arguments. | msozeau |
| 2006-10-24 | Ajout de la tactique 'remember' | herbelin |
| 2006-10-17 | Mise en forme des theories | notin |
| 2006-10-05 | revision de la semantique de rewrite ... in <clause>. details dans la doc | letouzey |
| 2006-09-22 | Ajout d'une valeur VList dans tacinterp pour permettre de cabler des | herbelin |
| 2006-09-21 | incomplete and temporary fix for PR#1222: revert accepts up to 10 args | letouzey |
| 2006-08-28 | Passage à une définition de inhabited plus dans les 'standard mathématique... | herbelin |
| 2006-06-25 | repetition d'hypotheses dans well_founded_induction_type_2 | letouzey |
| 2006-06-09 | Modification déf de exists! pour éviter une éta-expansion et pouvoir être... | herbelin |
| 2006-06-04 | Remplacement 'singleton' par 'unique' as a simple way to avoid a conflict wit... | herbelin |
| 2006-06-04 | Ajout exists! et restructuration/extension des fichiers sur la | herbelin |
| 2006-05-29 | Ajout d'alias pour prodT_rect et cie qui avaient été oublkÃiés | herbelin |
| 2006-05-28 | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin |
| 2006-04-28 | Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '... | notin |
| 2006-03-17 | Modification des propriétés (svn:executable) | notin |
| 2006-03-04 | Titres moins envahissants pour coqdoc | herbelin |
| 2006-02-27 | quelques raccourcis commodes + un f_equal plus efficace | letouzey |
| 2006-02-23 | Ajout 'exists! x:A, P (suite) | herbelin |
| 2006-02-23 | Ajout 'exists! x:A, P | herbelin |
| 2006-02-10 | code mort | herbelin |
| 2006-02-06 | Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et Ru... | herbelin |
| 2006-01-22 | Application de la suggestion de Nicolas Magaud (#1060) | herbelin |
| 2006-01-21 | Backtrack commit précédent: la préservation de l'énoncé exact Acc_ind es... | herbelin |
| 2006-01-21 | Préservation énoncé exact Acc_ind par choix nom 'a' comme paramètre de Acc | herbelin |
| 2006-01-19 | Correction associativité de IF et exists (visible à l'affichage uniquement ... | herbelin |
