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
*
On Linux, we read /proc/self/exe to get the executable's path instead
glondu
2007-09-28
*
Correction bug 1711
herbelin
2007-09-28
*
Oubli dans Setoid.v
notin
2007-09-28
*
Forget to update the CHANGES file
vsiles
2007-09-28
*
Modification of the Scheme command.
vsiles
2007-09-28
*
Découpage de Setoid.v
notin
2007-09-27
*
Reals: prod_f_SO inclut f(0) dans le produit et devient prod_f_R0
herbelin
2007-09-27
*
Complément aux commits 10124 et 10125 sur l'inférence de type (correction
herbelin
2007-09-26
*
added a lemma to prove inj_pair2 when eq_dec is available.
vsiles
2007-09-26
*
An update on theories/Numbers.
emakarov
2007-09-25
*
Changes in Backtrack documentation. More accurate.
courtieu
2007-09-25
*
Suppression de tous les alias de la forme x:=x dans la compilation du filtrage.
herbelin
2007-09-25
*
Added the documentation for Backtrack and BackTo.
courtieu
2007-09-24
*
curpat_ty was in a smaller context
msozeau
2007-09-21
*
Petit complément au commit 10131.
herbelin
2007-09-21
*
Correction d'un bug dans check + ajout de tests
notin
2007-09-21
*
Update on theories/Numbers
emakarov
2007-09-21
*
Update on theories/Numbers. Natural numbers are mostly complete,
emakarov
2007-09-21
*
- Fixing bug 1703 ("intros until n" falls back on the variable name when
herbelin
2007-09-21
*
Changed the definition of Nminus in BinNat.v by removing comparison.
emakarov
2007-09-20
*
Indication de quel type de constantes est dépliable dans "simpl" (cf
herbelin
2007-09-19
*
MAJ date copyright doc
herbelin
2007-09-18
*
Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)
herbelin
2007-09-18
*
Raffinement de l'algorithme d'inférence de type
herbelin
2007-09-17
*
Réponse à une incompatibilité introduite dans 10114 (calcul du nombre
herbelin
2007-09-16
*
* Adding compability with ocaml 3.10 + camlp5 (rework of
letouzey
2007-09-15
*
Correction du bug #1679 (congruence) et ajout test-suite
corbinea
2007-09-14
*
Update before joining all signatures into one.
emakarov
2007-09-13
*
- renaming Qle_shift_recip_r into Qle_shift_inv_r, etc
roconnor
2007-09-07
*
errors in recdef.ml4:
bertot
2007-09-06
*
this should fix a problem described in a message by Dufourd on July 30th, 2007
bertot
2007-09-06
*
Uniformisation politique de nommage evd/isevars (evd si evar_defs,
herbelin
2007-09-06
*
Itération sur les sous-termes dans la vérification de la condition de garde
herbelin
2007-09-06
*
fixed icons
barras
2007-09-04
*
fixed icons
barras
2007-09-04
*
Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte les
herbelin
2007-09-04
*
A word on the measure and wf modifiers
msozeau
2007-09-01
*
Suite commit 10103 (expansion des défs locales triviales dans l'étape
herbelin
2007-09-01
*
fin de la correction de Function
jforest
2007-08-31
*
correction bug d'efficacite dans Function
jforest
2007-08-31
*
Mise à jour des paramètres Whelp et ajouts d'options Set Whelp Server
herbelin
2007-08-30
*
Oubli dans commit 10102...
herbelin
2007-08-30
*
Prise en compte des redéfinitions de variables (définitions locales
herbelin
2007-08-29
*
- Débogueur: positionnement de set_detype_anonymous pour ne pas
herbelin
2007-08-29
*
Adding a few lemmas for reasoning about inequalities over the
roconnor
2007-08-28
*
Correction d'un bug dans check_and_warn
notin
2007-08-28
*
Oubli dans la révision 10098 (nettoyage body_of_type)
herbelin
2007-08-27
*
Suppression des type_app et body_of_type qui alourdissent inutilement le code
herbelin
2007-08-27
*
Fix bug on wellfounded defs with constant parameters and dependencies on the ...
msozeau
2007-08-26
*
Fix de Bruijn bug in wf definitions.
msozeau
2007-08-26
[next]