aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/romega/const_omega.ml
Commit message (Expand)AuthorAge
* 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
* Correction de bugs: coq_false et coq_true au lieu de coq_False et coq_trueGravatar 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
* Reparation ROmega V8/Omega ZERO/POS/NEGGravatar mohring2004-03-04
* adaptation V8 version Pierre CregutGravatar mohring2004-03-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
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* 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
* reparation ZneGravatar mohring2001-09-19
* Romega/names/MakefileGravatar mohring2001-09-18