index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
Commit message (
Expand
)
Author
Age
*
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
*
*** empty log message ***
werner
2002-04-17
*
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
*
Optimisation
desmettr
2002-04-02
*
Suppression PI_lb et PI_ub
desmettr
2002-04-02
*
Suppression Field
desmettr
2002-04-02
*
sans utiliser Field
desmettr
2002-03-29
*
Suppression des invocations a Field
desmettr
2002-03-29
*
Prise en compte des dependances dans la tactique Case
mohring
2002-03-26
*
*** empty log message ***
werner
2002-03-22
*
Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de Z...
herbelin
2002-03-22
*
Intuition ne fait plus de Unfold des constantes (il faut les faire
courant
2002-03-21
*
Intuition now takes an (optional) tactic as parameter. This tactic is
courant
2002-03-20
*
Exportation de SplitRmult et SplitAbsolu
delahaye
2002-03-19
*
Field ne fait maintenant que les reductions necessaires
delahaye
2002-03-17
*
Ajout de lemmes
mohring
2002-03-13
*
*** empty log message ***
desmettr
2002-03-07
*
petits changements afin de profiter du nouveau Rewrite/in
barras
2002-03-05
*
Nouveau Rewrite-in plus economique
barras
2002-03-04
*
Ajout andb_true_eq pour PolyList.list_beq
herbelin
2002-02-28
*
Doc + ajout fold_symmetric et nth_In
herbelin
2002-02-22
*
Doc
herbelin
2002-02-22
*
code mort dans tactinterp; plus de Debug On/Off dans Correctness
filliatr
2002-02-21
*
Uniformisation des theoremes dans Set et Type (def. de Acc_rect et
barras
2002-02-19
*
option -dump-glob pour coqdoc
filliatr
2002-02-14
*
Syntaxe IF then else au lieu de either and_then or_else
barras
2002-02-14
*
changement generation de schema d'elimination, False_rec est primitif, Constr...
mohring
2002-01-31
*
modification de la definition des def inductives unitaires et autorisation d'...
mohring
2002-01-29
*
Bug affichage de O (de nat) dans une expression sur Z
herbelin
2002-01-25
*
Zdiv et Zmod dans Zcomplements
filliatr
2002-01-25
*
Bug commentaire (*i i*)
herbelin
2002-01-18
*
amadouage de coqweb
letouzey
2002-01-18
*
ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de contr...
letouzey
2002-01-18
*
Modifs incongrues dans le précédent commit
herbelin
2002-01-10
*
MAJ des Id pour coqweb
herbelin
2002-01-09
*
Ajout en-tête
herbelin
2002-01-07
*
Passage coqweb
herbelin
2001-12-21
*
Commentaire coqweb non fermé
herbelin
2001-12-21
*
Extension de Even et Div2
herbelin
2001-12-21
*
*** empty log message ***
desmettr
2001-12-19
*
*** empty log message ***
desmettr
2001-12-07
*
*** empty log message ***
desmettr
2001-12-07
*
Amélioration nommage hypothèses NewInduction (et incompatibilités)
herbelin
2001-12-06
*
*** empty log message ***
desmettr
2001-12-05
[next]