index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
omega
Commit message (
Expand
)
Author
Age
*
Retour sur amendement de l'interprétation mult sur nat (bug 743) car incompa...
herbelin
2004-05-28
*
Correction interprétation mult sur nat (bug 743), bug Oufo (mais Oufo est de...
herbelin
2004-05-07
*
Reparation ROmega V8/Omega ZERO/POS/NEG
mohring
2004-03-04
*
Protection d'un 'clear' qui peut etre dependant
herbelin
2004-03-01
*
La correction precedente a mis en evidence un defaut de l'utilisation de intr...
herbelin
2003-12-24
*
Renommages des hypotheses transformees car en raison des possibles dependance...
herbelin
2003-12-23
*
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
barras
2003-12-15
*
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-11-29
*
Restructuration ZArith
herbelin
2003-11-12
*
Déport des lemmes de Omega de ZArith vers OmegaLemmas
herbelin
2003-11-05
*
Extension de zarith
herbelin
2003-11-04
*
Construction des chemins de constantes plus robuste
herbelin
2003-10-21
*
Cacher les .v8
herbelin
2003-10-03
*
Un peu plus de souplesse dans la globalisation des noms utilises par les tact...
herbelin
2003-09-26
*
Globalisation de ce qui n'etait pas encore globalise
herbelin
2003-06-10
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
commentaires
herbelin
2003-04-17
*
Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"
herbelin
2003-04-09
*
factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )
corbinea
2003-03-31
*
minus a changé d'emplacement -> omega pas content
letouzey
2003-03-31
*
*** empty log message ***
barras
2003-03-12
*
Auto with zarith essaye Abstract Omega sur un but False
filliatr
2003-01-30
*
Problèmes et améliorations divers affichage
herbelin
2002-12-09
*
Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...
herbelin
2002-10-23
*
Meilleure lisibilité grâce à tclTHENLIST
herbelin
2002-10-19
*
Réparation bug #180
herbelin
2002-10-19
*
Omega can now elim hyps of type False. Therefore, it knows how to deal
courant
2002-10-02
*
Un peu (plus) d'ordre dans Nametab...
coq
2002-09-24
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
ZArith_base, Zbool, Bool_nat
filliatr
2002-06-20
*
Protection des tactiques contre l'utilisation sans le bon contexte de thories
herbelin
2002-06-03
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.v
herbelin
2002-05-29
*
Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.v
herbelin
2002-05-29
*
Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml
herbelin
2002-04-11
*
Uniformisation convert_hyp
herbelin
2002-02-28
*
patch Omega (bug 129)
filliatr
2002-01-25
*
Correction de Pierre Crégut pour le bug MERGE_EQ
herbelin
2002-01-21
*
Bug MERGE_EQ
herbelin
2002-01-18
*
ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de contr...
letouzey
2002-01-18
*
compat ocaml 3.03
filliatr
2001-12-13
*
GROS COMMIT:
barras
2001-11-05
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Transparent
barras
2001-09-20
*
Nettoyage reduce_to_ind et one_step_reduce
herbelin
2001-09-09
*
Parsing
herbelin
2001-08-10
*
Expérimentation de NewDestruct et parfois NewInduction
herbelin
2001-08-05
*
correction bug Omega
filliatr
2001-07-05
*
remplace Zarith par ZArith
mohring
2001-04-19
*
portage exemples Correctness; changement du nom de pred_of_minus dans coq_omega
filliatr
2001-04-10
[next]