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
*
debug subst_command_placeholder : replace %s and not only %
jnarboux
2008-05-26
*
Réorganisation des points d'appui du undo de CoqIDE (type reset_info).
herbelin
2008-05-26
*
Encore un bug de undo
herbelin
2008-05-26
*
Résolution bug #1850 sur notations avec niveaux inconnus de
herbelin
2008-05-26
*
Fix bashism in doc generation.
glondu
2008-05-26
*
Bug undo CoqIDE sur End
herbelin
2008-05-26
*
the -g option is not recongnized in ocaml < 3.10.0
jforest
2008-05-26
*
- Nouvelle option "Set Printing Existential Instances" pour forcer
herbelin
2008-05-25
*
- Prise en compte des frozen state de Coq autant que possible pour
herbelin
2008-05-24
*
Ajout de la possibilité d'utiliser fix/cofix dans les notations.
herbelin
2008-05-24
*
doc of coqchk + improved module cache and computation of module sets
barras
2008-05-23
*
Cyclic31 : replace the ugly time-consuming brute-force proof by a reasonable ...
letouzey
2008-05-23
*
- Fix bug #1858, Hint Unfold calling the wrong locate function.
msozeau
2008-05-23
*
Nouvelle doc pour les modules.
soubiran
2008-05-23
*
(Not completely finished) proofs that int31 integers fulfill the CyclicAxioms...
letouzey
2008-05-23
*
Strategy commands are now exported
barras
2008-05-22
*
fixed dependency problems with the checker
barras
2008-05-22
*
writing a match on a digit via syntax "if ... then ... else" is not a good id...
letouzey
2008-05-22
*
Proposition for a almost-bitsize-independent Int31.v (joint work with J. Voui...
letouzey
2008-05-22
*
QRewrite is now obsolete. It was containing manual ltac stuff
letouzey
2008-05-22
*
Should fix the dependancy issue mentioned by J.Forest about NMake:
letouzey
2008-05-22
*
switch theories/Numbers from Set to Type (both the abstract and the bignum pa...
letouzey
2008-05-22
*
improved coqchk targets
barras
2008-05-22
*
added coqchk to the main Makefile and a make variable VALIDATE to check the v...
barras
2008-05-22
*
refined the conversion oracle
barras
2008-05-21
*
refined the conversion oracle
barras
2008-05-21
*
Désactivation affichage image coqide en attendant un barcelos
herbelin
2008-05-21
*
Correction bugs ide undo et highlight (suite à typos)
herbelin
2008-05-21
*
Correction d'un bug de l'unification pattern qui oubliait d'expanser
herbelin
2008-05-20
*
Corrections d'erreurs rapportées par Frédéric Besson sur le précédent
herbelin
2008-05-20
*
added checker to svn:ignore
barras
2008-05-20
*
also fixed conversion of the checker
barras
2008-05-20
*
Cleanup build_new, remove unneeded try-with and debug interaction of
msozeau
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
*
MAJ crédits
herbelin
2008-05-19
*
Intégration de micromega ("omicron" pour fourier et sa variante sur Z,
herbelin
2008-05-19
*
Fix globalization bug in class_tactics and refactorize instance
msozeau
2008-05-19
*
Fix caml debug flags configuration, -g works with the native compiler only
msozeau
2008-05-19
*
Minor improvement: group stuff about carry apart from stuff about zn2z
letouzey
2008-05-19
*
Thanks to Matthieu's commit 10941, Ad-hoc tactics contained in QRewrite are n...
letouzey
2008-05-19
*
ZModulo: Z viewed modulo 2^digits implements CyclicAxioms
letouzey
2008-05-17
*
Fix a de Bruijn bug in setoid_rewrite when rewriting under
msozeau
2008-05-17
*
Filename ZnZ (or Z_nZ in a later attempt) is neither pretty nor accurate
letouzey
2008-05-16
*
BigNum: more reorganization, mainly moves GenXYZ to DoubleXYZ
letouzey
2008-05-16
*
Deletion of empty directory TreeMod
letouzey
2008-05-16
*
ZTreeMod was meant to prove that BigZ correspond to the Integer Axioms.
letouzey
2008-05-16
*
More BigNum cleanup:
letouzey
2008-05-16
*
In practice, the new setoid rewrite (and the "at" syntax) allows to avoid
letouzey
2008-05-15
[next]