aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/omega
Commit message (Expand)AuthorAge
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
* Makefile: ml dependencies of contribs are moved to .mllib filesGravatar letouzey2009-03-14
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* Take advantage of natdynlink when available: almost all contribs become loada...Gravatar letouzey2008-12-16
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* small copy&paste bug in zify: some Pmult should be NmultGravatar letouzey2007-11-08
* A generic preprocessing tactic zify for (r)omegaGravatar letouzey2007-07-18
* Improvements / Bug fixes for ROmega Gravatar letouzey2007-07-09
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* suppression de code mort (avec bug de nom)Gravatar letouzey2006-11-16
* Bug suite déplacement Int.v dans ZArithGravatar herbelin2006-06-09
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...Gravatar notin2006-04-28
* correctifs de bug pour romega: Gravatar letouzey2006-03-23
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...Gravatar herbelin2005-12-26
* Adaptation des noms de OmegaLemmas aux noms de Z; traduction des noms v7 de Z...Gravatar herbelin2005-12-25
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Open Scope non Local malencontreuxGravatar herbelin2005-05-03
* Utilisation Z_scopeGravatar herbelin2005-05-02
* Déboggueur et code mortGravatar herbelin2005-02-18
* Correction bug #922 (problème dans depend) + formattage débogueurGravatar herbelin2005-02-17
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Bug transformation assert dans commit précédentGravatar herbelin2004-12-29
* Utilisation d'entiers en précision arbitraire pour le noyau d'omega (cf #898)Gravatar herbelin2004-12-27
* Remplacement du coeur d'omega (omega.ml) par la version plus gnrale utilise p...Gravatar herbelin2004-12-27
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* Nouvelle en-têteGravatar herbelin2004-07-16
* Retour sur amendement de l'interprétation mult sur nat (bug 743) car incompa...Gravatar herbelin2004-05-28
* Correction interprétation mult sur nat (bug 743), bug Oufo (mais Oufo est de...Gravatar herbelin2004-05-07
* Reparation ROmega V8/Omega ZERO/POS/NEGGravatar mohring2004-03-04
* Protection d'un 'clear' qui peut etre dependantGravatar herbelin2004-03-01
* La correction precedente a mis en evidence un defaut de l'utilisation de intr...Gravatar herbelin2003-12-24
* Renommages des hypotheses transformees car en raison des possibles dependance...Gravatar herbelin2003-12-23
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Restructuration ZArithGravatar herbelin2003-11-12
* Déport des lemmes de Omega de ZArith vers OmegaLemmasGravatar herbelin2003-11-05
* Extension de zarithGravatar herbelin2003-11-04
* Construction des chemins de constantes plus robusteGravatar herbelin2003-10-21
* Cacher les .v8Gravatar herbelin2003-10-03
* Un peu plus de souplesse dans la globalisation des noms utilises par les tact...Gravatar herbelin2003-09-26
* Globalisation de ce qui n'etait pas encore globaliseGravatar herbelin2003-06-10
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* commentairesGravatar herbelin2003-04-17
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"Gravatar herbelin2003-04-09
* factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )Gravatar corbinea2003-03-31