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
...
*
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
*
Échange des mots clés 'using' et 'with' en argument de 'firstorder' (wish #...
notin
2007-02-22
*
doc: typo/english: "is left associating" -> "is left-associative".
lmamane
2007-02-22
*
Documentation of tactical "t1 || t2": t2 is executed if t1 fails to
lmamane
2007-02-22
*
Utilisation de l'environnement pour l'affichage de certains messages d'erreurs
herbelin
2007-02-21
*
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
*
Removed some useless code in mod_typing that was redundant with safe_typing.
soubiran
2007-02-21
*
Fixed the pseudo-cicularity problem due to the with operator on Module Type.
soubiran
2007-02-21
*
Correct coq depend, add eq_rect elimination tactic to SubtacTactics
msozeau
2007-02-19
*
Ajouts de lemmes dans Min et Max
notin
2007-02-19
*
Various little subtac fixes, add some useful tactics.
msozeau
2007-02-19
*
Compilation de la FAQ
notin
2007-02-18
*
Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.
msozeau
2007-02-16
*
Add 'dest obj as pat in body' keyword as a pattern-matching shortcut.
msozeau
2007-02-16
*
Missing keyword
msozeau
2007-02-16
*
lift params appropriately, do not need to coerce to tycon
msozeau
2007-02-16
*
Add functionality to permit printing terms with references to anonymous varia...
msozeau
2007-02-16
*
Update implementation for dependent types. Works just as well as before for s...
msozeau
2007-02-16
*
Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lors
herbelin
2007-02-15
*
Réparation absence d'interprétation des liaisons vers listes
herbelin
2007-02-15
*
encodage des types
filliatr
2007-02-14
*
tactique yices
filliatr
2007-02-14
*
Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de
herbelin
2007-02-13
*
Bug mineur dans la generation des principes d'induction pour Function
jforest
2007-02-12
*
Autres passages de Set à Type dans Relations et Wellfounded
herbelin
2007-02-12
*
Fix matching on dependent types, taking a safe stand.
msozeau
2007-02-12
[prev]
[next]