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