index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
success
Commit message (
Expand
)
Author
Age
*
Forgot the test file.
msozeau
2008-03-15
*
Backtrack sur le test censé discriminer entre une erreur d'evar non
herbelin
2008-03-15
*
Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)
herbelin
2008-03-10
*
New implementation of Add Relation as a DefaultRelation instance
msozeau
2008-03-08
*
Fix bugs that were reopened due to the change of setoid
msozeau
2008-03-08
*
f_equal, revert, specialize in ML, contradict in better Ltac (+doc)
letouzey
2008-03-07
*
Correction d'un bug "ancestral": apply ne savait pas unifier ?n=?n
herbelin
2008-03-06
*
Correction d'une typo restant du commit 10557 et cause d'échec de contribs
herbelin
2008-03-05
*
congruence now knows about _ -> _
corbinea
2008-02-21
*
added products and sorts as possible heads for canonical structures
corbinea
2008-02-19
*
Added default canonical structures (see example in test-suite)
corbinea
2008-02-14
*
Correction d'un bug de clear
notin
2008-02-11
*
Correction d'un bug à l'interprétation de "change" (on exigeait que
herbelin
2008-02-06
*
Unification de TacLetRecIn et TacLetIn. En particulier, on peut
herbelin
2008-02-01
*
Debug implementation of dependent induction/dependent destruction and documen...
msozeau
2008-01-31
*
Work on dependent induction tactic and friends, finish the test-suite example
msozeau
2008-01-30
*
Ajout d'un test pour le mode déclaratif + test pour le bug #1776
notin
2008-01-23
*
Better resolution of implicit parameters in typeclass binders, add extensiona...
msozeau
2008-01-02
*
Complément aux commits 10124 et 10125 sur l'inférence de type (correction
herbelin
2007-09-26
*
Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)
herbelin
2007-09-18
*
Raffinement de l'algorithme d'inférence de type
herbelin
2007-09-17
*
Réponse à une incompatibilité introduite dans 10114 (calcul du nombre
herbelin
2007-09-16
*
Correction du bug #1679 (congruence) et ajout test-suite
corbinea
2007-09-14
*
Extension et documentation de real_clean/evar_define dans evarutil.ml:
herbelin
2007-08-25
*
Ajout d'un exemple d'inversion des dépendances dans le prédicat comme
herbelin
2007-08-10
*
Add a test case for the new "dependent" induction tactics.
msozeau
2007-08-08
*
A generic preprocessing tactic zify for (r)omega
letouzey
2007-07-18
*
Improvements / Bug fixes for ROmega
letouzey
2007-07-09
*
Contrôle de la compatibilité de apply via une information dans les
herbelin
2007-05-28
*
Unification suite: petits affinements pour préserver la compatibilité
herbelin
2007-05-24
*
Nouvelle stratégie d'unification des types des with-bindings dans
herbelin
2007-05-22
*
Wish #1582 (3eme)
herbelin
2007-05-18
*
Correction bug calcul des implicites en présence d'evars dans les types
herbelin
2007-05-16
*
Modification syntaxe de Test
herbelin
2007-04-30
*
Correction bug #1507 (report révision 9807 de v8.1 vers trunk)
herbelin
2007-04-29
*
Correction bug #1477 sur ordre des variables partagées par les or-patterns.
herbelin
2007-04-13
*
Test non régression bug #1491
herbelin
2007-04-13
*
Test de non-régression pour commit 9673
herbelin
2007-03-15
*
Correction typo liée au commit 8779 (levait une anomalie)
herbelin
2007-02-21
*
Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES
herbelin
2007-02-21
*
Réparation absence d'interprétation des liaisons vers listes
herbelin
2007-02-15
*
Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de
herbelin
2007-02-13
*
Report de la révision 9577 dans le trunk
notin
2007-02-01
*
Redondance erronée dans les tests
herbelin
2007-01-25
*
Correction d'un bug d'unification-pattern dans l'algo d'unification
herbelin
2007-01-22
*
Correction pour le rapport de bug #1325 par rétablissement du
herbelin
2007-01-22
*
Suite au mail de Lionel a propos du Makefile:
letouzey
2007-01-12
*
Alignement de la politique de renommage de rename_bound_var (utilisé pour
herbelin
2006-12-13
*
Dépliage du terme d'induction avant suppression quand celui-ci est un
herbelin
2006-12-13
*
Correction bug #1041 (double cause : non évitement des noms existants en
herbelin
2006-12-12
[next]