aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/romega/ReflOmegaCore.v
Commit message (Expand)AuthorAge
* ROmega : make it work even if no Require Import ZArith has been doneGravatar letouzey2008-07-16
* Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]Gravatar herbelin2008-05-09
* Ajout notation [ x ; ... ; y ] dans list_scope. Changement de laGravatar herbelin2008-04-29
* Verify Setoid is loaded only if we're not in Coq.Classes.*. Add explicitGravatar msozeau2008-04-09
* small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is Gravatar letouzey2007-11-06
* Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;Gravatar notin2007-08-16
* Big reorganization of romega/ReflOmegaCore.v: towards a modular Gravatar letouzey2007-07-10
* Improvements / Bug fixes for ROmega Gravatar letouzey2007-07-09
* mult_sym, plus_sym -> mult_comm, plus_commGravatar herbelin2006-11-19
* Ajout de quelques Arguments Scope pour simuler la récursivité du scope rome...Gravatar herbelin2006-07-11
* correctifs de bug pour romega: Gravatar letouzey2006-03-23
* 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
* - changement ordre arguments interp_goal_concl pour permettre applicationGravatar herbelin2005-02-21
* 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
* *** empty log message ***Gravatar barras2003-03-12
* MAJGravatar herbelin2003-01-22
* Simplification de Simplify (plus de ())Gravatar herbelin2003-01-19
* 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
* ZArith_base, Zbool, Bool_natGravatar filliatr2002-06-20
* RomegaGravatar mohring2001-09-20
* Romega/names/MakefileGravatar mohring2001-09-18