aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* + ameliorating the tactic "functional induction"Gravatar jforest2006-06-06
* Fusion if.v et If.v (MacOS X ne sait pas distinguer la casse)Gravatar herbelin2006-05-31
* Fusion destruct.v et Destruct.v (MacOS X ne sait pas distinguer la casseGravatar herbelin2006-05-31
* Adaptation au passage de vector dans TypeGravatar herbelin2006-05-28
* Adaptation au passage de option dans TypeGravatar herbelin2006-05-28
* encore un exemple ne marchant pas, ni avec omega ni avec romegaGravatar letouzey2006-05-22
* tests de RomegaGravatar letouzey2006-05-19
* Centralisation de la détection lettre/symbole par le lexeur dans les plages ...Gravatar herbelin2006-05-10
* Vieux bug de fin 2004 gardé pour mémoireGravatar herbelin2006-05-05
* Ajout bug #1102Gravatar herbelin2006-04-28
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...Gravatar notin2006-04-28
* Tests notationsGravatar herbelin2006-04-15
* - Correction bug calcul mind_consnrealargs, introduit à la révisionGravatar herbelin2006-03-22
* Ajout test relatif au bug #984Gravatar herbelin2006-03-05
* Ajout test bug 1089Gravatar herbelin2006-03-02
* Correction du bug 808: il est maintenant interdit de déclarer une assomption...Gravatar coq2006-03-02
* Correction bug #842 (rename d'une hyp du contexte)Gravatar herbelin2006-03-01
* Prise en compte coercions autour des sous-termes filtrés (si non dépendants)Gravatar herbelin2006-01-30
* Répercussion mise à jour de Pierre Casteran vis à vis du changement de sta...Gravatar herbelin2006-01-23
* Test bug 983Gravatar herbelin2006-01-20
* Test utf-8Gravatar herbelin2006-01-15
* Test conflictuel - ajouté pour mémoireGravatar herbelin2006-01-11
* Test or-patternsGravatar herbelin2006-01-11
* Test bug #1025Gravatar herbelin2005-12-30
* Mini-test d'extractionGravatar herbelin2005-12-27
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
* Activation du test de Refine en v7 pour mémoire avant passage à la v8Gravatar herbelin2005-12-21
* *** empty log message ***Gravatar mohring2005-11-03
* Test reproductibilité du bug #1031Gravatar herbelin2005-11-02
* Declare Implicit TacticGravatar herbelin2005-09-09
* Suppression test CCSolve car remplaçé par Congruence mais qui ne traite pas...Gravatar herbelin2005-09-09
* Test clear final dans intros patternGravatar herbelin2005-09-08
* A wish by Bas Spitters granted: a little more of unification up toGravatar sacerdot2005-05-19
* Implemented autorewrite with ... in hyp [using ...].Gravatar sacerdot2005-05-18
* Ajout Unset Implicit Arguments manquantGravatar herbelin2005-03-21
* Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des hyps...Gravatar herbelin2005-03-20
* Ajout test bug #935Gravatar herbelin2005-03-19
* Nouvelle syntaxe 'with' des modules non gérée en v7Gravatar herbelin2005-03-17
* Nouvelle syntaxe 'with' des modules non gérée en v7Gravatar herbelin2005-03-16
* Fix bug #931: leave dependent evars as such for refineGravatar herbelin2005-03-08
* *** empty log message ***Gravatar herbelin2005-02-21
* Test bug #922Gravatar herbelin2005-02-17
* test de la bonne position des vars de ltac entre les vars et les relsGravatar herbelin2005-02-02
* The new tutorial on (co)inductive types by Pierre Casteran.Gravatar sacerdot2005-01-12
* Ajout bug do_restrict_hypGravatar herbelin2004-12-08
* Erreur commit précédentGravatar herbelin2004-12-06
* Ajout bug #888Gravatar herbelin2004-12-06
* Ajout bug #889Gravatar herbelin2004-12-06
* Failed in 8.0pl1Gravatar herbelin2004-12-04
* Was failing in 8.0pl1Gravatar herbelin2004-12-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 00:21:52 +0000