aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Le calcul de la classe dans class_args_of ne suivait pas celui de class_ofGravatar herbelin2006-10-21
* Correction d'un vieux bug de coercion avec éta-expansion (utilisationGravatar herbelin2006-10-21
* Clarification des contraintes sur le contexte de paramètres desGravatar herbelin2006-10-17
* Adaptation des tests suite à la modification de Rewrite .. in (r9201)Gravatar notin2006-10-13
* Correction test-suite suite à r9186Gravatar notin2006-10-13
* Exemple avec liaison des variables de filtrage du matchGravatar herbelin2006-10-09
* Notations:Gravatar herbelin2006-10-09
* suite commit 9222 : rétablissement des tests autre que complexitéGravatar herbelin2006-10-06
* Ajout d'un répertoire de test de la complexitéGravatar herbelin2006-10-06
* Correction de deux cas où les types inductifs n'étaient pas comparésGravatar herbelin2006-10-05
* nouveau ring/fieldGravatar barras2006-10-02
* Une passe sur l'injection et la discrimination...Gravatar herbelin2006-10-01
* Corrections mineuresGravatar notin2006-09-25
* Correction d'un bug de coercion de pattern introduit dans la 8.1betaGravatar herbelin2006-09-23
* Correction bug #1179 (result of Notation.decompose_notation_key in wrong orderGravatar herbelin2006-09-23
* Wish #1187 granted (support for canonical structures that are recordsGravatar herbelin2006-09-23
* Correction bug #1229 (toplevel "unresolved evar" fled throughGravatar herbelin2006-09-23
* - Correction filtrage des notations impliquant un "match" : la présenceGravatar herbelin2006-09-23
* Test Tactic NotationGravatar herbelin2006-09-22
* Report de l'heuristique d'unification premier ordre flexible/rigideGravatar herbelin2006-09-15
* Correction du bug #1181Gravatar jforest2006-09-14
* Ajout unification pattern dans l'algorithme d'unification desGravatar herbelin2006-09-12
* Extension et réorganisation de l'interprétation des (co-)points fixesGravatar herbelin2006-09-01
* Diverses modifications autour de l'unification modulo conversion:Gravatar herbelin2006-08-28
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
* remove an orphan comment (attached to a piece of code that was removed).Gravatar bertot2006-08-22
* Checks that abstract setoid rings can be defined in a module and the tacticGravatar bertot2006-08-17
* Correction bug 1172 + correction en passant de la taille des paramètres de f...Gravatar herbelin2006-07-07
* functional inversion now takes a quatified hypothesis as first argumentGravatar jforest2006-07-04
* - completely new version of "functional inversion" using inversion onGravatar jforest2006-07-04
* Test des motifs disjonctifs multiplesGravatar herbelin2006-07-03
* Correction bug #1182 (ajout refresh_universe car le polymorphisme de sorte de...Gravatar herbelin2006-06-27
* Stricte positivité en présence de types inductifs imbriqués avec paramètr...Gravatar herbelin2006-06-23
* modifs de test-suite suite au passage des graphes de Function dans TypeGravatar jforest2006-06-23
* Deux vérifications que le polymorphisme de sorte des inductifs ne fonctionne...Gravatar herbelin2006-06-22
* Adaptation Tactics.out et Cases.out au comportement actuel à défaut d'évit...Gravatar herbelin2006-06-09
* + 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 sig2 dans TypeGravatar herbelin2006-05-28
* 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
* Correction trou de typage des éliminations d'inductifs introduit dans commit...Gravatar herbelin2006-05-13
* Conformité nouveaux principes: Declare Module non utilisable pour définir u...Gravatar herbelin2006-05-10
* 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