aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
2008-10-14test-suite: more utf8 tests, a test of ! ? and so on in rewritesletouzey
2008-10-03Minor fixes related to coqdoc and --interpolate and the dependentmsozeau
2008-09-15Report improvements in Equations to the dependent elimination tactic:msozeau
2008-09-13Finish debugging the unification machinery in [Equations]. Do the _compmsozeau
2008-09-12Add a type argument to letin_tac instead of using casts and recomputingmsozeau
2008-09-11Fixes in dependent induction tactic, putting things in better order formsozeau
2008-09-11Some more debugging of [Equations], unification still not perfect.msozeau
2008-09-07More debugging of [Equations], now able to discharge even the heavilymsozeau
2008-09-03Correct handling of implicit arguments in [Equations] definitions,msozeau
2008-09-02Add support for recursive definitions to [Equations], deciding if amsozeau
2008-09-02Initial implementation of a new command to define (dependent) functions bymsozeau
2008-09-02Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutherbelin
2008-08-05Correction de bugs:herbelin
2008-07-22Correct implementation of discharging of implicit arguments and add newmsozeau
2008-07-11Correction d'un autre bug autour de la gestion des niveaux vides deherbelin
2008-07-07Fix implicit arguments in sections bug and check for resolution of evars whenmsozeau
2008-06-29Préférence donnée aux constantes qui ne sont pas des projectionsherbelin
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
2008-06-18Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkherbelin
2008-06-10- Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.herbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-05-30Improve the dependent induction tactic to automatically find themsozeau
2008-05-26Résolution bug #1850 sur notations avec niveaux inconnus deherbelin
2008-05-20Retrait d'un test commité par erreur en 10947herbelin
2008-05-19Intégration de micromega ("omicron" pour fourier et sa variante sur Z,herbelin
2008-05-15Various fixes:msozeau
2008-05-14Résolution des problèmes ambigus d'inférence du type de retour desherbelin
2008-05-05Mise en place d'un algorithme d'inversion des contraintes de type lorsherbelin
2008-05-01Clarification de l'ordre d'interprétation des variables dans ltac. Enherbelin
2008-04-30Contournement laborieux de la "feature" de camlp5 qui entrainait leherbelin
2008-04-28Petites corrections vis à vis des commits 10860, 10859, 10850herbelin
2008-04-27Quelques bricoles autour de l'unification:herbelin
2008-04-25Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveherbelin
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-15- Un peu de doc, préparation du CHANGES pour la release.herbelin
2008-04-14Fix setoid tests, use red for a Setoid_Theory lemma, and Parametricmsozeau
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-04Correction problème de compil (blast.ml)herbelin
2008-04-03Chgts mineurs:herbelin
2008-04-02Minor fixes. Use expanded type in class_tactics for Morphism search, tomsozeau
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2008-03-29Fix test-suite files, change conflicting notation "->rel" and the othersmsozeau
2008-03-28Improve error handling and messages for typeclasses. msozeau
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
2008-03-26Diverses petites modifs dans la test-suite:notin
2008-03-16Misc: Add test for bug 1704, now closed. Add usual syntax for lists inmsozeau
2008-03-15Forgot the test file.msozeau
2008-03-15Backtrack sur le test censé discriminer entre une erreur d'evar nonherbelin
2008-03-10Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)herbelin
2008-03-08New implementation of Add Relation as a DefaultRelation instancemsozeau