aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/field
Commit message (Expand)AuthorAge
* Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;Gravatar notin2007-08-16
* fixed field_simplify + changed precedence of let and fun in ltacGravatar barras2006-10-30
* Noms de compatibilité déplacés en bloc à la fin du fichierGravatar herbelin2006-10-26
* MénageGravatar notin2006-10-25
* oopsGravatar barras2006-10-25
* conflit de nom (Field_theory) modulo la casseGravatar barras2006-10-25
* Correction sym -> commGravatar herbelin2006-10-19
* typo doc + bug legacy fieldGravatar barras2006-10-16
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...Gravatar notin2006-04-28
* Exploitation du 'let rec' + présentationGravatar herbelin2006-03-05
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...Gravatar herbelin2005-12-26
* Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...Gravatar herbelin2005-12-21
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* Nouvelle en-têteGravatar herbelin2004-07-16
* reals: renamed type option into field_rel_optionGravatar marche2004-03-11
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* petits changements de syntaxeGravatar barras2003-11-12
* nouvelle syntaxe de ltacGravatar barras2003-10-16
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* Cacher les .v8Gravatar herbelin2003-10-03
* Ajout fonctions syntaxe v8 pour contrib MapleModeGravatar herbelin2003-09-23
* Système de renommage des noms de tactiques LtacGravatar herbelin2003-09-22
* Passage à la V8 par défautGravatar herbelin2003-09-22
* Pour accomoder autant le printer v8 que v7Gravatar herbelin2003-09-06
* Protection contre les types sans corps associéGravatar herbelin2003-09-06
* Suppression définitive de lmatch et or_metanum dans tacinterpGravatar herbelin2003-05-21
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Explicitation arguments de eqGravatar herbelin2003-04-11
* Mauvaise resolution conflit dans commit precedentGravatar herbelin2003-04-07
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Légères simplifications code de Field; message d'erreur si pas égalitéGravatar herbelin2003-04-03
* remplace == par = dans la tactique field pour que le debugger marche a nouvea...Gravatar narboux2003-04-01
* Fail 1 pour traverser le matchGravatar herbelin2003-04-01
* Plus de eqT; message FailGravatar herbelin2003-03-31
* factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )Gravatar corbinea2003-03-31
* *** empty log message ***Gravatar barras2003-03-12
* Utilisation de 'Recursive' pour les tactiques récursivesGravatar herbelin2003-01-20
* Restructuration interpréteur de tactique: plus d'évaluation partielle à la...Gravatar herbelin2003-01-19
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* MAJ syntaxeGravatar herbelin2002-11-14
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Protection des tactiques contre l'utilisation sans le bon contexte de thoriesGravatar herbelin2002-06-03
* Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vGravatar herbelin2002-05-29
* Fix d'un bug sur le test des inversesGravatar delahaye2002-03-19