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
...
*
Bug (destruct/induction ne savent pas traiter le cas non atomique avec paramÃ...
herbelin
2004-01-27
*
maj
filliatr
2004-01-27
*
maj
filliatr
2004-01-27
*
deplacement des cma et cmxa dans les sous-repertoires
barras
2004-01-26
*
reparation de qqs bugs du traducteur
barras
2004-01-26
*
a try to make intro patterns better
bertot
2004-01-26
*
maj
filliatr
2004-01-26
*
maj
filliatr
2004-01-26
*
streamlines the keywords for definitions, require commandsbinders, notation
bertot
2004-01-24
*
maj
filliatr
2004-01-24
*
MAJ
herbelin
2004-01-23
*
Bug induction lors de types inductives avec parametres
herbelin
2004-01-23
*
maj
filliatr
2004-01-23
*
change add path commands to get the extra argument and the Hint commands
bertot
2004-01-22
*
Correction lecture des locations si pas demandees dans l'ordre
herbelin
2004-01-22
*
Protection table des locations lors de Load (pour coqdoc)
herbelin
2004-01-22
*
fixes argument lists for tactic definitions, updates inversion tactics
bertot
2004-01-22
*
adds a clause argument to symmetry
bertot
2004-01-22
*
corrects the way the structural argument declaration is handled in
bertot
2004-01-22
*
adds the notations in inductive definitions, improves the consistency between
bertot
2004-01-22
*
handles explicit function calls, names meta variables in patterns
bertot
2004-01-22
*
maj
filliatr
2004-01-22
*
maj
filliatr
2004-01-22
*
MAJ
herbelin
2004-01-21
*
Export information des references et location de notations pour coqdoc
herbelin
2004-01-21
*
Export information des references de notations pour coqdoc
herbelin
2004-01-21
*
Deplacement lexer pour dependance dans constrintern
herbelin
2004-01-21
*
updates the structure of fix (struct argument added) and if
bertot
2004-01-21
*
MAJ
herbelin
2004-01-21
*
maj
filliatr
2004-01-21
*
coqide utf8
marche
2004-01-20
*
Le traducteur utilisait un afficheur des reels obsolete et bugge
herbelin
2004-01-20
*
Suppression 'Implicit Arguments On/Off' qui n'a plus lieu d'etre en v8
herbelin
2004-01-20
*
maj
filliatr
2004-01-20
*
handles projector notations, cases with return types,
bertot
2004-01-19
*
1.20
bertot
2004-01-19
*
1.19
bertot
2004-01-19
*
adds constructs to handle notations in patterns
bertot
2004-01-19
*
maj
filliatr
2004-01-19
*
maj
filliatr
2004-01-17
*
ajoute une option -linkall dans compilation de bin/parser pour assurer que
bertot
2004-01-16
*
Corrige: Intros [] etait traduit intros (), qui ne reparse pas
barras
2004-01-16
*
maj
filliatr
2004-01-16
*
translation to structures now okay for pattern matching constructs
bertot
2004-01-15
*
Ajout nouvelles options
herbelin
2004-01-15
*
Ajout load-vernac-source-verbose
herbelin
2004-01-15
*
maj
filliatr
2004-01-15
*
maj
filliatr
2004-01-15
*
compact nested universal quantifications into a single quantification with
bertot
2004-01-14
*
make sure the parser for FORMULA does not require them to be enclosed in
bertot
2004-01-14
[prev]
[next]