| Age | Commit message (Expand) | Author |
|---|
| 2008-09-14 | Fix bug #1931 by searching for a sort after doing beta,iota,delta- | msozeau |
| 2008-09-13 | Finish debugging the unification machinery in [Equations]. Do the _comp | msozeau |
| 2008-09-12 | Add a type argument to letin_tac instead of using casts and recomputing | msozeau |
| 2008-09-11 | Fixes in dependent induction tactic, putting things in better order for | msozeau |
| 2008-09-11 | Some more debugging of [Equations], unification still not perfect. | msozeau |
| 2008-09-07 | Skip complexity tests on demand | glondu |
| 2008-09-07 | More debugging of [Equations], now able to discharge even the heavily | msozeau |
| 2008-09-03 | Fix bug #1935, reworking the reflexivity, symmetry... tactics to use | msozeau |
| 2008-09-03 | Correct handling of implicit arguments in [Equations] definitions, | msozeau |
| 2008-09-02 | Add support for recursive definitions to [Equations], deciding if a | msozeau |
| 2008-09-02 | Initial implementation of a new command to define (dependent) functions by | msozeau |
| 2008-09-02 | Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about | herbelin |
| 2008-08-18 | Renaming parser -> coq-parser | glondu |
| 2008-08-07 | micromega : bug fixes and optimisations | fbesson |
| 2008-08-05 | Correction de bugs: | herbelin |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-07-29 | Oops... the trunk behaviour is different | glondu |
| 2008-07-29 | Update test-suite output | glondu |
| 2008-07-28 | Fix bashism in test-suite/check | glondu |
| 2008-07-25 | Correction d'une incohérence de typage des inductifs polymorphes: les | herbelin |
| 2008-07-25 | A better test for relations being setoids or not: do leibniz rewrite iff | msozeau |
| 2008-07-22 | Add test-suite file for bug# 1905 and minor fix in Program/Equality. | msozeau |
| 2008-07-22 | Correct implementation of discharging of implicit arguments and add new | msozeau |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2008-07-11 | Correction d'un autre bug autour de la gestion des niveaux vides de | herbelin |
| 2008-07-09 | test-suite/complexity/ring2.v: Zeqb_ok -> Zbool.Zeq_bool_eq | letouzey |
| 2008-07-07 | Fix implicit arguments in sections bug and check for resolution of evars when | msozeau |
| 2008-07-07 | Micromega: doc + test-suite update | fbesson |
| 2008-07-03 | Prise en compte de changments dans subtac | notin |
| 2008-07-02 | Improved robustness of micromega parser. Proof search of Micromega test-suite... | fbesson |
| 2008-07-01 | Documentation Prop<=Set et Arguments Scope Global | herbelin |
| 2008-06-29 | Préférence donnée aux constantes qui ne sont pas des projections | herbelin |
| 2008-06-25 | Micromega : bugs fixes - renaming of tactics - documentation | fbesson |
| 2008-06-21 | - Implantation de la suggestion 1873 sur discriminate. Au final, | herbelin |
| 2008-06-18 | Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk | herbelin |
| 2008-06-10 | - Amélioration nommage dans EqdepFacts suivant remarque de Arthur C. | herbelin |
| 2008-06-10 | - Correct handling of DependentMorphism error, using tclFAIL instead of | msozeau |
| 2008-06-09 | - Documentation de admit et Print Assumptions. | herbelin |
| 2008-06-08 | - Extension de "generalize" en "generalize c as id at occs". | herbelin |
| 2008-06-05 | Renommage id dans le test Nametab (suite ajout d'une constante de ce | herbelin |
| 2008-06-03 | Temporarily disabling automatic test for bug 1338.v | notin |
| 2008-05-30 | Improve the dependent induction tactic to automatically find the | msozeau |
| 2008-05-29 | fixed bug #1780: a lift was missing (match predicate) | barras |
| 2008-05-28 | - Correction bug highlighting "Module" dans Coqide | herbelin |
| 2008-05-26 | Résolution bug #1850 sur notations avec niveaux inconnus de | herbelin |
| 2008-05-22 | Strategy commands are now exported | barras |
| 2008-05-21 | Correction bugs ide undo et highlight (suite à typos) | herbelin |
| 2008-05-20 | Corrections d'erreurs rapportées par Frédéric Besson sur le précédent | herbelin |
| 2008-05-20 | Léger backtrack sur commit coqide précédent (si la commande à annuler | herbelin |
| 2008-05-20 | Fixed coqide bug #1856 that was introduced in revision 10915. | herbelin |
