aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/romega
Commit message (Expand)AuthorAge
* 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
* Traduction des noms v7 de Z en noms v8Gravatar herbelin2005-12-25
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Pas de dépendance en OmegaGravatar herbelin2005-02-21
* Correction de bugs: coq_false et coq_true au lieu de coq_False et coq_trueGravatar herbelin2005-02-21
* - changement ordre arguments interp_goal_concl pour permettre applicationGravatar herbelin2005-02-21
* - Correction de bugsGravatar herbelin2005-02-21
* Standardisation of function names about global references (especially, renami...Gravatar herbelin2005-02-18
* 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
* Nouvelle en-têteGravatar herbelin2004-07-16
* Reparation ROmega V8/Omega ZERO/POS/NEGGravatar mohring2004-03-04
* adaptation V8 version Pierre CregutGravatar mohring2004-03-03
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Renommage canonique d'un lemme redondantGravatar herbelin2003-11-05
* Renommage canonique d'un lemme redondantGravatar herbelin2003-11-05
* Cacher les .v8Gravatar herbelin2003-10-03
* Un peu plus de souplesse dans la globalisation des noms utilises par les tact...Gravatar herbelin2003-09-26
* Branchement constant sur CoqlibGravatar herbelin2003-09-12
* *** empty log message ***Gravatar barras2003-03-12
* MAJGravatar herbelin2003-01-22
* Simplification de Simplify (plus de ())Gravatar herbelin2003-01-19
* Problèmes et améliorations divers affichageGravatar herbelin2002-12-09
* Remplacement de Syntactic Definition par NotationGravatar herbelin2002-11-24
* Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...Gravatar herbelin2002-10-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* ZArith_base, Zbool, Bool_natGravatar filliatr2002-06-20
* Protection des tactiques contre l'utilisation sans le bon contexte de thoriesGravatar herbelin2002-06-03
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vGravatar herbelin2002-05-29
* Prise en compte des corps de letin dans les hypothèsesGravatar herbelin2002-03-01
* convert_hyp a change de typeGravatar barras2002-03-01
* compat ocaml 3.03Gravatar filliatr2001-12-13
* GROS COMMIT:Gravatar barras2001-11-05
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...Gravatar herbelin2001-10-12
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* RomegaGravatar mohring2001-09-20
* MAJ V7.1Gravatar herbelin2001-09-19
* reparation ZneGravatar mohring2001-09-19
* Romega/names/MakefileGravatar mohring2001-09-18