index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
Commit message (
Expand
)
Author
Age
*
Renaming parser -> coq-parser
glondu
2008-08-18
*
micromega : bug fixes and optimisations
fbesson
2008-08-07
*
Correction de bugs:
herbelin
2008-08-05
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Oops... the trunk behaviour is different
glondu
2008-07-29
*
Update test-suite output
glondu
2008-07-29
*
Fix bashism in test-suite/check
glondu
2008-07-28
*
Correction d'une incohérence de typage des inductifs polymorphes: les
herbelin
2008-07-25
*
A better test for relations being setoids or not: do leibniz rewrite iff
msozeau
2008-07-25
*
Add test-suite file for bug# 1905 and minor fix in Program/Equality.
msozeau
2008-07-22
*
Correct implementation of discharging of implicit arguments and add new
msozeau
2008-07-22
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
Correction d'un autre bug autour de la gestion des niveaux vides de
herbelin
2008-07-11
*
test-suite/complexity/ring2.v: Zeqb_ok -> Zbool.Zeq_bool_eq
letouzey
2008-07-09
*
Fix implicit arguments in sections bug and check for resolution of evars when
msozeau
2008-07-07
*
Micromega: doc + test-suite update
fbesson
2008-07-07
*
Prise en compte de changments dans subtac
notin
2008-07-03
*
Improved robustness of micromega parser. Proof search of Micromega test-suite...
fbesson
2008-07-02
*
Documentation Prop<=Set et Arguments Scope Global
herbelin
2008-07-01
*
Préférence donnée aux constantes qui ne sont pas des projections
herbelin
2008-06-29
*
Micromega : bugs fixes - renaming of tactics - documentation
fbesson
2008-06-25
*
- Implantation de la suggestion 1873 sur discriminate. Au final,
herbelin
2008-06-21
*
Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk
herbelin
2008-06-18
*
- Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.
herbelin
2008-06-10
*
- Correct handling of DependentMorphism error, using tclFAIL instead of
msozeau
2008-06-10
*
- Documentation de admit et Print Assumptions.
herbelin
2008-06-09
*
- Extension de "generalize" en "generalize c as id at occs".
herbelin
2008-06-08
*
Renommage id dans le test Nametab (suite ajout d'une constante de ce
herbelin
2008-06-05
*
Temporarily disabling automatic test for bug 1338.v
notin
2008-06-03
*
Improve the dependent induction tactic to automatically find the
msozeau
2008-05-30
*
fixed bug #1780: a lift was missing (match predicate)
barras
2008-05-29
*
- Correction bug highlighting "Module" dans Coqide
herbelin
2008-05-28
*
Résolution bug #1850 sur notations avec niveaux inconnus de
herbelin
2008-05-26
*
Strategy commands are now exported
barras
2008-05-22
*
Correction bugs ide undo et highlight (suite à typos)
herbelin
2008-05-21
*
Corrections d'erreurs rapportées par Frédéric Besson sur le précédent
herbelin
2008-05-20
*
Léger backtrack sur commit coqide précédent (si la commande à annuler
herbelin
2008-05-20
*
Fixed coqide bug #1856 that was introduced in revision 10915.
herbelin
2008-05-20
*
Retrait d'un test commité par erreur en 10947
herbelin
2008-05-20
*
Intégration de micromega ("omicron" pour fourier et sa variante sur Z,
herbelin
2008-05-19
*
Various fixes:
msozeau
2008-05-15
*
Résolution des problèmes ambigus d'inférence du type de retour des
herbelin
2008-05-14
*
MAJ et bricoles diverses
herbelin
2008-05-12
*
Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757
herbelin
2008-05-07
*
Mise en place d'un algorithme d'inversion des contraintes de type lors
herbelin
2008-05-05
*
Clarification de l'ordre d'interprétation des variables dans ltac. En
herbelin
2008-05-01
*
Contournement laborieux de la "feature" de camlp5 qui entrainait le
herbelin
2008-04-30
*
Backtrack on using metas eagerly in auto, only done in "new auto" for
msozeau
2008-04-28
*
Petites corrections vis à vis des commits 10860, 10859, 10850
herbelin
2008-04-28
*
Quelques bricoles autour de l'unification:
herbelin
2008-04-27
[next]