index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Mise en place d'ensembles de notations symboliques pour nat, Z et R
herbelin
2002-10-13
*
Nettoyage
herbelin
2002-10-13
*
Déplacement de + et * aux niveaux de précédence 7 et 6
herbelin
2002-10-13
*
Déplacement de + et * aux niveaux de précédence 7 et 6
herbelin
2002-10-13
*
Première proposition d'un type ML exprimant la syntaxe de constr; nettoyage
herbelin
2002-10-13
*
Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...
herbelin
2002-10-13
*
réparation de la protection contre les clauses indiscernables de TACTIC EXTE...
herbelin
2002-10-12
*
Notation 2:Check et 2:Eval
herbelin
2002-10-12
*
Restriction sur la forme des Syntactic Definition et re-localisation en fonct...
herbelin
2002-10-12
*
Nettoyage
herbelin
2002-10-12
*
Forcer la réouverture d'un fichier explicitement requis même si le
herbelin
2002-10-12
*
maj
filliatr
2002-10-11
*
Ajout ClassicalFacts
herbelin
2002-10-10
*
gestion coherente de l'option -R et des Require A.B.C.
barras
2002-10-10
*
Nametab permet de definir le meme truc la deuxieme fois
coq
2002-10-10
*
retour en arriere concernant la recherche d'occurence modulo expansion des le...
barras
2002-10-09
*
Preuve du lemme de Rolle
desmettr
2002-10-09
*
MAJ pour modification dans Rcomplet
desmettr
2002-10-09
*
Suppression d'un lemme redondant
desmettr
2002-10-09
*
Proof of Heine's theorem
desmettr
2002-10-09
*
maj
filliatr
2002-10-09
*
Subst ne fait pas clear sur x:=e
filliatr
2002-10-08
*
maj
filliatr
2002-10-08
*
Une fonction de moins dans .mli
coq
2002-10-07
*
Lazy manuelles dans le code
coq
2002-10-07
*
*** empty log message ***
desmettr
2002-10-07
*
*** empty log message ***
courant
2002-10-07
*
Quelques resultats complementaires
desmettr
2002-10-07
*
Affaiblissement des hypotheses dans TAF_gen
desmettr
2002-10-07
*
Make sure that bin/parser exists when checking that it works
bertot
2002-10-07
*
maj
filliatr
2002-10-07
*
correcting the treatment of many tactics that use quant_hyp in file xlate.ml
bertot
2002-10-06
*
Lazy experimentale temporaire...
coq
2002-10-05
*
pretty s'appellait prettyp mais il est revenu sous son ancien nom
herbelin
2002-10-05
*
Ajout du lemme derivable_pt_lim_power
desmettr
2002-10-04
*
Preuve de Bolzano-Weierstrass
desmettr
2002-10-04
*
Re-introduce the treatement of Tacticals that Hugo had already done in
bertot
2002-10-04
*
Intégration des modifs de la V7.3.1
herbelin
2002-10-03
*
Previous version did compile but did not make it possible to actually run
bertot
2002-10-03
*
Simplification suite MAJ 3.06
herbelin
2002-10-03
*
maj
filliatr
2002-10-03
*
Changements Omega
courant
2002-10-02
*
*** empty log message ***
desmettr
2002-10-02
*
Fonctions Ln et puissance
desmettr
2002-10-02
*
debian pkg now recommends proof general
courant
2002-10-02
*
Omega can now elim hyps of type False. Therefore, it knows how to deal
courant
2002-10-02
*
maj
filliatr
2002-10-02
*
Adding the congruence closure tactics (CC and CCsolve).
corbinea
2002-10-01
*
Oops...
coq
2002-10-01
*
backslahs foireux
filliatr
2002-10-01
[next]