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
*
code mort
herbelin
2006-02-10
*
maj
coq
2006-02-09
*
very minor bug correction and cleanning
bertot
2006-02-09
*
securing intros (we now use h_intro)
bertot
2006-02-09
*
Minor bugs fixes
bertot
2006-02-09
*
maj
coq
2006-02-08
*
Changing Set to Type for iter.
bertot
2006-02-08
*
One can use a measure {mes f x} instead of a well-founded relation in GenFixp...
bertot
2006-02-08
*
Julien:
bertot
2006-02-08
*
Localisation des erreurs de sorte du prétypage
herbelin
2006-02-08
*
Ajout bibliothèque String de Laurent Théry
herbelin
2006-02-08
*
Ajout bibliothèque String de Laurent Théry
herbelin
2006-02-08
*
maj
coq
2006-02-07
*
oubli de code de debugging
herbelin
2006-02-07
*
Messages nth branche
herbelin
2006-02-07
*
Idem numbering of 'Unfold', 'simpl', ...
herbelin
2006-02-07
*
Amélioration des messages d'erreurs de tacred; unfold considère maintenant le
herbelin
2006-02-07
*
Ajout plural
herbelin
2006-02-07
*
Mise en conformité de l'ordre des occurrences de pattern avec l'affichage
herbelin
2006-02-07
*
MAJ
herbelin
2006-02-07
*
maj
coq
2006-02-06
*
Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et Ru...
herbelin
2006-02-06
*
warning seulement si mode verbose
herbelin
2006-02-06
*
coq_makefile
herbelin
2006-02-06
*
Ajout de l'essai d'effacement des noms des cibles custom par la cible clean
herbelin
2006-02-06
*
maj
coq
2006-02-05
*
Debugging en syntaxe v8
herbelin
2006-02-05
*
maj
coq
2006-02-04
*
Branchement sur nouvelle interface de declare_numeral_interpreter
herbelin
2006-02-04
*
Recherche des global_reference paresseusement pour pouvoir interpréter
herbelin
2006-02-04
*
parsing/g_ascii_syntax.ml
herbelin
2006-02-04
*
Ajout nat_path et find_reference
herbelin
2006-02-04
*
Utilisation du section_path pour le parsing des notations primitives,
herbelin
2006-02-04
*
code mort
herbelin
2006-02-04
*
maj
coq
2006-02-03
*
added mli 's for the nex functional induction (forgotten last time).
coq
2006-02-03
*
+ Adding an error message when the function cannot be defined
bertot
2006-02-03
*
maj
coq
2006-02-02
*
maj
coq
2006-02-01
*
protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)
barras
2006-02-01
*
protect ring operations when passed to gen_phiZ and gen_phiN (abstract rings)
barras
2006-02-01
*
New version of functional induction / inversion. By Julien Forest,
coq
2006-02-01
*
Optimisation filtrage sans lieurs (utile pour Ltac)
herbelin
2006-02-01
*
maj
coq
2006-01-31
*
Adaptation message d'erreur au cas des string
herbelin
2006-01-31
*
Ajout de fichiers d'interprétation de la syntaxe primitive pour string et char
herbelin
2006-01-31
*
Ajout décidabilité
herbelin
2006-01-31
*
maj
coq
2006-01-30
*
Suppression fonctions d'interprétation du vieux Case
herbelin
2006-01-30
*
Prise en compte coercions autour des sous-termes filtrés (si non dépendants)
herbelin
2006-01-30
[next]