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
*
Ajout test relatif au bug #984
herbelin
2006-03-05
*
Ajout test bug 1089
herbelin
2006-03-02
*
Correction du bug 808: il est maintenant interdit de déclarer une assomption...
coq
2006-03-02
*
Correction bug #842 (rename d'une hyp du contexte)
herbelin
2006-03-01
*
Prise en compte coercions autour des sous-termes filtrés (si non dépendants)
herbelin
2006-01-30
*
Répercussion mise à jour de Pierre Casteran vis à vis du changement de sta...
herbelin
2006-01-23
*
Test bug 983
herbelin
2006-01-20
*
Test utf-8
herbelin
2006-01-15
*
Test conflictuel - ajouté pour mémoire
herbelin
2006-01-11
*
Test or-patterns
herbelin
2006-01-11
*
Test bug #1025
herbelin
2005-12-30
*
Mini-test d'extraction
herbelin
2005-12-27
*
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
herbelin
2005-12-21
*
Activation du test de Refine en v7 pour mémoire avant passage à la v8
herbelin
2005-12-21
*
*** empty log message ***
mohring
2005-11-03
*
Test reproductibilité du bug #1031
herbelin
2005-11-02
*
Declare Implicit Tactic
herbelin
2005-09-09
*
Suppression test CCSolve car remplaçé par Congruence mais qui ne traite pas...
herbelin
2005-09-09
*
Test clear final dans intros pattern
herbelin
2005-09-08
*
A wish by Bas Spitters granted: a little more of unification up to
sacerdot
2005-05-19
*
Implemented autorewrite with ... in hyp [using ...].
sacerdot
2005-05-18
*
Ajout Unset Implicit Arguments manquant
herbelin
2005-03-21
*
Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des hyps...
herbelin
2005-03-20
*
Ajout test bug #935
herbelin
2005-03-19
*
Nouvelle syntaxe 'with' des modules non gérée en v7
herbelin
2005-03-17
*
Nouvelle syntaxe 'with' des modules non gérée en v7
herbelin
2005-03-16
*
Fix bug #931: leave dependent evars as such for refine
herbelin
2005-03-08
*
*** empty log message ***
herbelin
2005-02-21
*
Test bug #922
herbelin
2005-02-17
*
test de la bonne position des vars de ltac entre les vars et les rels
herbelin
2005-02-02
*
The new tutorial on (co)inductive types by Pierre Casteran.
sacerdot
2005-01-12
*
Ajout bug do_restrict_hyp
herbelin
2004-12-08
*
Erreur commit précédent
herbelin
2004-12-06
*
Ajout bug #888
herbelin
2004-12-06
*
Ajout bug #889
herbelin
2004-12-06
*
Failed in 8.0pl1
herbelin
2004-12-04
*
Was failing in 8.0pl1
herbelin
2004-12-03
*
Ajout test dependent rewrite
herbelin
2004-10-27
*
reflexivity, symmetry, symmetry ... in e transitivity now fall-back
sacerdot
2004-10-14
*
New commands
sacerdot
2004-10-07
*
Added "as ..." parameter to Add Morphism.
sacerdot
2004-10-04
*
Added "as ..." parameters to "Add Setoid"
sacerdot
2004-10-01
*
New tactic
sacerdot
2004-09-30
*
New tactic [setoid_]rewrite ... in ... [generate side conditions ...].
sacerdot
2004-09-30
*
Test updated.
sacerdot
2004-09-29
*
Ajouts
herbelin
2004-09-25
*
Ajout bug #255
herbelin
2004-09-24
*
* New test (for setoid_replace in the general case)
sacerdot
2004-09-03
*
* setoid_test.v removed and added again in new syntax
sacerdot
2004-09-03
*
The previous test file was truncated. New commit to fix the previous
sacerdot
2004-08-23
[next]