index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Init
Commit message (
Expand
)
Author
Age
*
Bug de précédence
herbelin
2002-07-15
*
Hack pour parser '{x:T|P}*B' sans parentheses
herbelin
2002-07-11
*
Utilisation d'Infix/Distfix autant que possible
herbelin
2002-05-29
*
petite erreur de syntaxe
barras
2002-05-14
*
ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewrite
barras
2002-05-14
*
lemmes plus_O_n et plus_Sn_m (pour Yves)
filliatr
2002-05-07
*
lemmes plus_O_n et plus_Sn_m (pour Yves)
filliatr
2002-05-07
*
Uniformisation (Qed/Save et Implicits Arguments)
herbelin
2002-04-17
*
Doc
herbelin
2002-02-22
*
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
*
Modifs incongrues dans le précédent commit
herbelin
2002-01-10
*
MAJ des Id pour coqweb
herbelin
2002-01-09
*
Suppression d'Export redondants
herbelin
2001-11-14
*
Suppression de Logic_Type.sigT, redondant avec Specif.sigT
herbelin
2001-10-24
*
and_rec redondant
letouzey
2001-09-27
*
Transparent
barras
2001-09-20
*
Deplacement des setoides.
clrenard
2001-09-19
*
Modification de l'emplacement des fichiers pour les setoides.
clrenard
2001-09-18
*
Fin de la modif Exc/option
mohring
2001-08-30
*
ajout option , Exc --> option, et lemmes dans les theories
mohring
2001-08-29
*
Expérimentation de NewDestruct et parfois NewInduction
herbelin
2001-08-05
*
Correction d'un bug du pretty-print
clrenard
2001-05-29
*
Modification pour passage p-automates
mohring
2001-05-15
*
documentation automatique de la bibliothèque standard
filliatr
2001-04-11
*
Introduction d'une preuve de False_rec
mohring
2001-03-30
*
entetes
filliatr
2001-03-15
*
Bug d'affichage à cause des << ... >>
herbelin
2000-12-21
*
separation calcul des implicites et declaration des constantes / inductifs / ...
filliatr
2000-11-21
*
Bug dans la règle de syntaxe de ex2
herbelin
2000-11-20
*
Modification de la table des tactic Definitions pour eviter l'ecriture
mohring
2000-11-07
*
Changement/extension dans les noms de parseurs de Grammar
herbelin
2000-11-07
*
Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d...
herbelin
2000-10-18
*
Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...
herbelin
2000-07-28
*
Bug affichage Error et Value
herbelin
2000-04-30
*
t -> $t dans regle grammaire EX
filliatr
2000-03-10
*
gros commit de tout ce que j'ai fait pendant les vacances :
filliatr
2000-01-21
*
Renommage command en constr
herbelin
2000-01-07
*
erreurs de syntax :$
filliatr
1999-12-16
*
- méthode load sur les Hints
filliatr
1999-12-13
*
fichiers prelude Coq
filliatr
1999-12-13