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
...
*
Support for implicit formal argument types in Program ; parse types in type s...
msozeau
2007-03-28
*
Modification de la vm:
notin
2007-03-27
*
Make multiple patterns work again with Program while simplifying the code.
msozeau
2007-03-26
*
stupid me: ?f two times in a pattern
letouzey
2007-03-26
*
PositiveOrderedTypeBits is now formulated to be a UsualOrderedType, not only ...
letouzey
2007-03-26
*
Correction des bugs #1455 et #1456
notin
2007-03-22
*
Remove debugging code committed by accident
lmamane
2007-03-22
*
A tentative fix for bug #1455
lmamane
2007-03-22
*
Suppression des sauts de lignes superflus de Show Script (test-suite/output/T...
notin
2007-03-21
*
Correction bug affichage des notations des noms de fonctions appliquées
herbelin
2007-03-20
*
Some tactic fixes in Subtac, fix obvious bug in admit_obligations but still a...
msozeau
2007-03-20
*
ajout contrib/dp/Dp.vo
filliatr
2007-03-20
*
traces Ergo
filliatr
2007-03-20
*
Forgot to update to new cast
msozeau
2007-03-19
*
Add a parameter to QuestionMark evar kind to say it can be turned into an obl...
msozeau
2007-03-19
*
Un chouia de portabilité en plus et pas de test si pas de bogomips
herbelin
2007-03-19
*
MAJ test complexité pour considérer le cas d'un temps avec un nombre
herbelin
2007-03-17
*
Correction du bug #1441
notin
2007-03-16
*
r11153@tannat: jforest | 2007-03-16 10:25:55 +0100
jforest
2007-03-16
*
Test de non-régression pour commit 9673
herbelin
2007-03-15
*
Typos
herbelin
2007-03-15
*
Suppression argument pattern_source du case_info (code jamais utilisé)
herbelin
2007-03-15
*
Prévention notations récursives sans terminal à gauche et qui font boucler
herbelin
2007-03-15
*
Add destruct_call variant where naming of introduced hypotheses is possible. ...
msozeau
2007-03-15
*
Add destruct_call_concl in SubtacTactics and fix obvious obligation handling ...
msozeau
2007-03-14
*
Bug dans Makefile (COQINSTALLPREFIX)
notin
2007-03-14
*
Removed an unnecessary argument (p : positive) in Prect_base.
emakarov
2007-03-14
*
Solve obligation handling bug of trying to solve automatically at Next Obliga...
msozeau
2007-03-13
*
Correction bug #1439 (comportement de replace by)
notin
2007-03-13
*
Proof simplification for eq_nat_dec et le_lt_dec: induction over
letouzey
2007-03-12
*
correction du bug 1432
jforest
2007-03-11
*
Remove bugguy notations
msozeau
2007-03-11
*
bug#1434 importing fonctor arguments, now it works.
soubiran
2007-03-09
*
Create a program_scope in subtac Utils
msozeau
2007-03-08
*
Add Program keywords to coqwc
msozeau
2007-03-08
*
Transparence de eq_dec et lt_dec daans OrderedTypeFacts
notin
2007-03-08
*
Application suggestion #1430 de Yevgeniy pour TEXINPUTS
herbelin
2007-03-07
*
màj dépendances .v: SubtacTactics.vo
lmamane
2007-03-06
*
FSetInterface: new item choose_equal in the spec S (request of P. Casteran)
letouzey
2007-02-28
*
The right tactics for definitions using measures.
msozeau
2007-02-28
*
Fix wf bug from F. Besson and work on ineqs generation.
msozeau
2007-02-27
*
Revision of the coqide configuration:
letouzey
2007-02-27
*
Correction d'un bug de l'install (win)
notin
2007-02-27
*
Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...
herbelin
2007-02-24
*
Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)
herbelin
2007-02-24
*
Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)
herbelin
2007-02-24
*
Améliorations utiles pour les Makefile répartis sur plusieurs répertoires
herbelin
2007-02-24
*
Opacity parameterization for obligations working.
msozeau
2007-02-24
*
Debug wellfounded defs, work on cleaning obls envs
msozeau
2007-02-23
*
Ajout fonction clenv_conv_leq pour résoudre les pbs de la forme
herbelin
2007-02-22
[prev]
[next]