index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
ZArith
Commit message (
Expand
)
Author
Age
*
Concentration des notations officielles dans Init/Notations; restructuration ...
herbelin
2003-05-21
*
coqide: toolbar/autosave
monate
2003-05-07
*
Ajout Open Scope
herbelin
2003-04-09
*
Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"
herbelin
2003-04-09
*
Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".
herbelin
2003-04-09
*
Pas d'associativité gauche au niveau 3 en vieille syntaxe !
herbelin
2003-03-28
*
notations <>, Assumption avec existentiel, replace term
mohring
2003-03-28
*
*** empty log message ***
barras
2003-03-21
*
*** empty log message ***
barras
2003-03-12
*
Modifications dans une tactique toplevel
delahaye
2003-02-13
*
Bug precedence
herbelin
2003-01-22
*
Adaptation à la nouvelle sémantique plus uniforme de "Match term"
herbelin
2003-01-21
*
bit vectors
filliatr
2003-01-06
*
Re-installation nombres dans les motifs sur Z
herbelin
2002-12-28
*
Ajout syntaxe '>'
herbelin
2002-12-15
*
Compatibilite times1 (suite)
herbelin
2002-12-10
*
Nouvelle preuve de times_convert pour nouvelle définition de times
herbelin
2002-12-09
*
Compatibilité times1
herbelin
2002-12-07
*
Un axiome en attendant la mise a jour de la preuve de times_convert
herbelin
2002-12-06
*
Amélioration sensible de l'efficacité de la multiplication
herbelin
2002-12-06
*
Z_scope doit annuler l'affichage de = entre
herbelin
2002-12-02
*
Correction affichage entiers en cas d'échec
herbelin
2002-11-26
*
Rétablissement affichage des entiers de nat
herbelin
2002-11-25
*
Traitement des parenthèses de nat au niveau du printer
herbelin
2002-11-24
*
Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...
herbelin
2002-11-24
*
Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pour
herbelin
2002-10-23
*
Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...
herbelin
2002-10-22
*
Mise en place d'ensembles de notations symboliques pour nat, Z et R
herbelin
2002-10-13
*
Affaiblissement de l'ordre sur Z on demande x < y et seulement
mohring
2002-09-25
*
Making the sumbool functions transparent, so that they can used to
bertot
2002-07-09
*
ZArith_base, Zbool, Bool_nat
filliatr
2002-06-20
*
deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwf
filliatr
2002-06-19
*
Adding file theories/ZArith/Zsqrt.v that contains a square root function.
bertot
2002-06-07
*
Correction non reconnaissance des variables de section dans les afficheurs de...
herbelin
2002-06-06
*
affaiblissement hyp de Zmult_reg_left
filliatr
2002-06-05
*
Contournement des My_special_variable
herbelin
2002-05-29
*
suppression de inf_decidable dans ZArith_dec (pour SeachPattern)
filliatr
2002-05-16
*
encore des lemmes sur Zdiv
filliatr
2002-05-14
*
nouveaux lemmes dans Zdiv (Claude Marche)
filliatr
2002-05-14
*
Cosmétique
herbelin
2002-05-06
*
lemmes sur Zdiv/Zmod
filliatr
2002-04-19
*
un thm de plus dans Zdiv; un retour chariot apres un message de la tactique F...
filliatr
2002-04-19
*
Quelques bugs avec inject_nat
herbelin
2002-04-17
*
Uniformisation (Qed/Save et Implicits Arguments)
herbelin
2002-04-17
*
Zdiv -> Export ZArith
filliatr
2002-04-08
*
syntaxe pour Zdiv et Zmod
filliatr
2002-04-08
*
simplification preuve
filliatr
2002-04-05
*
nouveau module Zdiv
filliatr
2002-04-05
*
Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de Z...
herbelin
2002-03-22
*
petits changements afin de profiter du nouveau Rewrite/in
barras
2002-03-05
[next]