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
...
*
Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte les
herbelin
2007-09-04
*
A word on the measure and wf modifiers
msozeau
2007-09-01
*
Suite commit 10103 (expansion des défs locales triviales dans l'étape
herbelin
2007-09-01
*
fin de la correction de Function
jforest
2007-08-31
*
correction bug d'efficacite dans Function
jforest
2007-08-31
*
Mise à jour des paramètres Whelp et ajouts d'options Set Whelp Server
herbelin
2007-08-30
*
Oubli dans commit 10102...
herbelin
2007-08-30
*
Prise en compte des redéfinitions de variables (définitions locales
herbelin
2007-08-29
*
- Débogueur: positionnement de set_detype_anonymous pour ne pas
herbelin
2007-08-29
*
Adding a few lemmas for reasoning about inequalities over the
roconnor
2007-08-28
*
Correction d'un bug dans check_and_warn
notin
2007-08-28
*
Oubli dans la révision 10098 (nettoyage body_of_type)
herbelin
2007-08-27
*
Suppression des type_app et body_of_type qui alourdissent inutilement le code
herbelin
2007-08-27
*
Fix bug on wellfounded defs with constant parameters and dependencies on the ...
msozeau
2007-08-26
*
Fix de Bruijn bug in wf definitions.
msozeau
2007-08-26
*
Add info on measure based defs.
msozeau
2007-08-26
*
Fix evars bug in mutual fixpoints with implicit types and bug in inequalities...
msozeau
2007-08-26
*
Add more equality tactics. Upgrade program_simpl for discrimination of conjun...
msozeau
2007-08-26
*
Extension et documentation de real_clean/evar_define dans evarutil.ml:
herbelin
2007-08-25
*
Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et -recty...
herbelin
2007-08-24
*
Utilisation plus précise de la contrainte de type pour interpréter les
herbelin
2007-08-24
*
Correction du bug #1634 + ajout de bugs dans la test-suite
notin
2007-08-22
*
Save IS NOT the same Defined ....
msozeau
2007-08-22
*
- Correction bug dans syntaxe des match (liste de motifs vide était acceptée)
herbelin
2007-08-22
*
Ajout d'un warning losrqu'un nom de bibliothèque est ambigü
notin
2007-08-22
*
Modification de l'initialisation des chemins de la librairie standard
notin
2007-08-20
*
Typo in INSTALL instructions
lmamane
2007-08-20
*
Erreur de copier/coller dans la section Guarded
notin
2007-08-20
*
Correction du bug #1322
notin
2007-08-16
*
Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;
notin
2007-08-16
*
An update on axiomatic number classes.
emakarov
2007-08-13
*
Correction (partielle) bug #1052 (coqdoc supprime les fins de ligne après un...
notin
2007-08-13
*
Correction du bug #1635
notin
2007-08-13
*
Ajout d'un exemple d'inversion des dépendances dans le prédicat comme
herbelin
2007-08-10
*
- Correction d'un bug de de Bruijn dans abstract_predicate (lié au
herbelin
2007-08-10
*
Typo
notin
2007-08-10
*
Modification de la test suite pour intégrer des tests spécifiques aux
notin
2007-08-10
*
Modification de control_only_guard, qui utilise maintenant
notin
2007-08-09
*
Fix dependency bugs due to Program modules renamings.
msozeau
2007-08-08
*
Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.v
emakarov
2007-08-08
*
Add a test case for the new "dependent" induction tactics.
msozeau
2007-08-08
*
A better Program documentation. Include it in the generated stdlib doc.
msozeau
2007-08-08
*
Move Program tactics into a proper theories/ directory as they are general pu...
msozeau
2007-08-07
*
Add a new tactic to generalize an instantiated inductive predicate adding equ...
msozeau
2007-08-07
*
Build system: _really_ don't recurse into VCS metadata for file lists
lmamane
2007-08-07
*
Build system:
lmamane
2007-08-07
*
Build system: BSD compatibility: do not use -printf action of find
lmamane
2007-08-01
*
mul and sqrt
thery
2007-07-30
*
Corrected the reference to glob.dump, which is used to create stdlib/index-bo...
emakarov
2007-07-26
*
Add glob.dump to Makefile the recommended way and document the
lmamane
2007-07-25
[prev]
[next]