aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2008-08-18Renaming parser -> coq-parserglondu
2008-08-07micromega : bug fixes and optimisationsfbesson
2008-08-05Correction de bugs:herbelin
2008-08-04Évolutions diverses et variées.herbelin
2008-07-29Oops... the trunk behaviour is differentglondu
2008-07-29Update test-suite outputglondu
2008-07-28Fix bashism in test-suite/checkglondu
2008-07-25Correction d'une incohérence de typage des inductifs polymorphes: lesherbelin
2008-07-25A better test for relations being setoids or not: do leibniz rewrite iffmsozeau
2008-07-22Add test-suite file for bug# 1905 and minor fix in Program/Equality.msozeau
2008-07-22Correct implementation of discharging of implicit arguments and add newmsozeau
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-07-11Correction d'un autre bug autour de la gestion des niveaux vides deherbelin
2008-07-09test-suite/complexity/ring2.v: Zeqb_ok -> Zbool.Zeq_bool_eqletouzey
2008-07-07Fix implicit arguments in sections bug and check for resolution of evars whenmsozeau
2008-07-07Micromega: doc + test-suite updatefbesson
2008-07-03Prise en compte de changments dans subtacnotin
2008-07-02Improved robustness of micromega parser. Proof search of Micromega test-suite...fbesson
2008-07-01Documentation Prop<=Set et Arguments Scope Globalherbelin
2008-06-29Préférence donnée aux constantes qui ne sont pas des projectionsherbelin
2008-06-25Micromega : bugs fixes - renaming of tactics - documentationfbesson
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-10- Correct handling of DependentMorphism error, using tclFAIL instead ofmsozeau
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-05Renommage id dans le test Nametab (suite ajout d'une constante de ceherbelin
2008-06-03Temporarily disabling automatic test for bug 1338.vnotin
2008-05-30Improve the dependent induction tactic to automatically find themsozeau
2008-05-29fixed bug #1780: a lift was missing (match predicate)barras
2008-05-28- Correction bug highlighting "Module" dans Coqideherbelin
2008-05-26Résolution bug #1850 sur notations avec niveaux inconnus deherbelin
2008-05-22Strategy commands are now exportedbarras
2008-05-21Correction bugs ide undo et highlight (suite à typos)herbelin
2008-05-20Corrections d'erreurs rapportées par Frédéric Besson sur le précédentherbelin
2008-05-20Léger backtrack sur commit coqide précédent (si la commande à annulerherbelin
2008-05-20Fixed coqide bug #1856 that was introduced in revision 10915.herbelin
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-12MAJ et bricoles diversesherbelin
2008-05-07Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757herbelin
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-28Backtrack on using metas eagerly in auto, only done in "new auto" formsozeau
2008-04-28Petites corrections vis à vis des commits 10860, 10859, 10850herbelin
2008-04-27Quelques bricoles autour de l'unification:herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 14:35:14 +0000