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
*
Verify Setoid is loaded before doing anything.
msozeau
2008-04-09
*
Fixes in new Morphisms files.
msozeau
2008-04-09
*
Fix evar bugs in type classes:
msozeau
2008-04-09
*
contradict can now handle False hypothesis in the spirit of contradiction
letouzey
2008-04-09
*
Correction bug List.map2 dans Case12.v
herbelin
2008-04-09
*
Fix the last compilation problem
msozeau
2008-04-09
*
Fix compilation problem
msozeau
2008-04-09
*
correction of bug 1829
jforest
2008-04-08
*
- A little cleanup in Classes/*. Separate standard morphisms on
msozeau
2008-04-08
*
Ajout d'options a coqdoc pour l'entete html
notin
2008-04-08
*
Fix big de Bruijn bug in mutually recursive definitions.
msozeau
2008-04-07
*
Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt :
herbelin
2008-04-06
*
Suite 10760
herbelin
2008-04-05
*
- Retour en arrière sur la capacité du nouvel apply à utiliser les
herbelin
2008-04-05
*
Minor fixes:
msozeau
2008-04-05
*
Mise en place d'une extension de apply pour que celui-ci sache
herbelin
2008-04-04
*
A file that can be loaded when a migration from Set to Type is desired
letouzey
2008-04-04
*
Correction problème de compil (blast.ml)
herbelin
2008-04-04
*
- Relâchement de la contrainte de bonne longueur des intropatterns
herbelin
2008-04-04
*
Test make 3.81
herbelin
2008-04-04
*
Quelques améliorations des intro patterns:
herbelin
2008-04-04
*
Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quand
herbelin
2008-04-04
*
- Amélioration de la présentation de RIneq, même si un nettoyage des
herbelin
2008-04-04
*
Protection de rewrite in contre le dépliage des constantes dans w_unify, ce qui
herbelin
2008-04-04
*
Essai d'un peu plus de conversion dans apply : suppression de la
herbelin
2008-04-03
*
New file FMapFullAVL containing the balancing proofs about FMapAVL:
letouzey
2008-04-03
*
Correction bug 1818, 3eme commentaire. mauvaise generation de substitution a ...
soubiran
2008-04-03
*
- Correction d'un bug de coq_makefile sur les variables CAMLLIBS et
notin
2008-04-03
*
Rework of FMapAVL inspired by recent changes of FSetAVL:
letouzey
2008-04-03
*
Chgts mineurs:
herbelin
2008-04-03
*
Patch sur le typage d'un foncteur applique a un alias.
soubiran
2008-04-03
*
Minor fixes. Use expanded type in class_tactics for Morphism search, to
msozeau
2008-04-02
*
Add the ability to specify the implicit status of section variables and
msozeau
2008-04-02
*
Typo affichage "simple apply"
herbelin
2008-04-01
*
Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient
herbelin
2008-04-01
*
Ajout "simple apply" et "simple eapply" pour apply sans unfold
herbelin
2008-04-01
*
Finish enhancemenent of return clause inference from tycons, integrating
msozeau
2008-04-01
*
Enhance handling of parameters in typeclass constraints: permit to specify an...
msozeau
2008-04-01
*
Add option to set the opacity of obligations to transparent, to be able
msozeau
2008-04-01
*
Correction du bug #1819
notin
2008-04-01
*
- Fix for rewriting under dependent products.
msozeau
2008-03-31
*
Suite commit 10730: MAJ xlate.ml
herbelin
2008-03-30
*
Modifications diverses et variées :
herbelin
2008-03-30
*
Ajout d'abbréviations/notations paramétriques
herbelin
2008-03-30
*
Fix test-suite files, change conflicting notation "->rel" and the others
msozeau
2008-03-29
*
Improve error handling and messages for typeclasses.
msozeau
2008-03-28
*
- Second pass on implementation of let pattern. Parse "let ' par [as x]?
msozeau
2008-03-28
*
Correction du bug 1816 (ajout d'un lemme dans Znat) et suppression
notin
2008-03-28
*
- notations &&& and ||| equivalent to andb and orb,
letouzey
2008-03-27
*
Various fixes on typeclasses:
msozeau
2008-03-27
[next]