index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
recdef
Age
Commit message (
Expand
)
Author
2006-02-09
Minor bugs fixes
bertot
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-03
+ Adding an error message when the function cannot be defined
bertot
2006-01-28
Réorganisation de la structure interne des types de déclarations (decl_kinds)
herbelin
2006-01-21
Messages de idtac et fail peuvent maintenant être des listes de string, int ...
herbelin
2006-01-18
Recursive Definition now supports functions with more than one argument.
coq
2006-01-12
Changing well founded induction to fix on accessibility proof in order
bertot
2006-01-11
removes several warnings in contrib/interface
bertot
2005-12-26
Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...
herbelin
2005-12-02
Changement des named_context
gregoire
2005-11-14
avoids warnings about unused variables
bertot
2005-11-07
Adds tools to help in defining new general recursive functions
bertot
[prev]