aboutsummaryrefslogtreecommitdiff
path: root/contrib/romega/ReflOmegaCore.v
AgeCommit message (Expand)Author
2006-11-19mult_sym, plus_sym -> mult_comm, plus_commherbelin
2006-07-11Ajout de quelques Arguments Scope pour simuler la récursivité du scope rome...herbelin
2006-03-23correctifs de bug pour romega: letouzey
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...herbelin
2005-12-25Traduction des noms v7 de Z en noms v8herbelin
2005-02-21- changement ordre arguments interp_goal_concl pour permettre applicationherbelin
2004-03-03adaptation V8 version Pierre Cregutmohring
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-11-05Renommage canonique d'un lemme redondantherbelin
2003-11-05Renommage canonique d'un lemme redondantherbelin
2003-03-12*** empty log message ***barras
2003-01-22MAJherbelin
2003-01-19Simplification de Simplify (plus de ())herbelin
2002-11-24Remplacement de Syntactic Definition par Notationherbelin
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...herbelin
2002-06-20ZArith_base, Zbool, Bool_natfilliatr
2001-09-20Romegamohring
2001-09-18Romega/names/Makefilemohring