aboutsummaryrefslogtreecommitdiff
path: root/contrib/omega
AgeCommit message (Expand)Author
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...herbelin
2003-11-12Restructuration ZArithherbelin
2003-11-05Déport des lemmes de Omega de ZArith vers OmegaLemmasherbelin
2003-11-04Extension de zarithherbelin
2003-10-21Construction des chemins de constantes plus robusteherbelin
2003-10-03Cacher les .v8herbelin
2003-09-26Un peu plus de souplesse dans la globalisation des noms utilises par les tact...herbelin
2003-06-10Globalisation de ce qui n'etait pas encore globaliseherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-04-17commentairesherbelin
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
2003-03-31factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )corbinea
2003-03-31minus a changé d'emplacement -> omega pas contentletouzey
2003-03-12*** empty log message ***barras
2003-01-30Auto with zarith essaye Abstract Omega sur un but Falsefilliatr
2002-12-09Problèmes et améliorations divers affichageherbelin
2002-10-23Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...herbelin
2002-10-19Meilleure lisibilité grâce à tclTHENLISTherbelin
2002-10-19Réparation bug #180herbelin
2002-10-02Omega can now elim hyps of type False. Therefore, it knows how to dealcourant
2002-09-24Un peu (plus) d'ordre dans Nametab...coq
2002-08-02Modules dans COQ\!\!\!\!coq
2002-06-20ZArith_base, Zbool, Bool_natfilliatr
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vherbelin
2002-05-29Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vherbelin
2002-04-11Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.mlherbelin
2002-02-28Uniformisation convert_hypherbelin
2002-01-25patch Omega (bug 129)filliatr
2002-01-21Correction de Pierre Crégut pour le bug MERGE_EQherbelin
2002-01-18Bug MERGE_EQherbelin
2002-01-18ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de contr...letouzey
2001-12-13compat ocaml 3.03filliatr
2001-11-05GROS COMMIT:barras
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-09-20Transparentbarras
2001-09-09Nettoyage reduce_to_ind et one_step_reduceherbelin
2001-08-10Parsingherbelin
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-07-05correction bug Omegafilliatr
2001-04-19remplace Zarith par ZArithmohring
2001-04-10portage exemples Correctness; changement du nom de pred_of_minus dans coq_omegafilliatr
2001-04-08Ajout lemmes arithmetiquesmohring
2001-03-28amelioration de la structure des universbarras
2001-03-15entetesfilliatr
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
2001-02-16ident au lieu de string pour le nom de base de qualidherbelin
2001-02-14Renommage des variables dans les schémas d'inductionherbelin
2001-02-14Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 06:14:15 +0000