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
...
*
Tests de référence circulaire au sous-typage de module (pour mémoire)
herbelin
2007-01-19
*
Update installation instructions to the modern world a bit.
lmamane
2007-01-18
*
Update for v8.1
lmamane
2007-01-18
*
Move definition of VO_TOOLS_DEP before first use of it.
lmamane
2007-01-17
*
Reintroduce compatibility with old versions of GNU make
lmamane
2007-01-17
*
Correction bug #1282
herbelin
2007-01-17
*
Correction bug #1302
herbelin
2007-01-17
*
Correction adresse CoRN dans FAQ (suite)
herbelin
2007-01-17
*
Correction adresse CoRN dans FAQ (cf #1317)
herbelin
2007-01-17
*
README update:
lmamane
2007-01-17
*
Various subtac fixes.
msozeau
2007-01-15
*
Suite au mail de Lionel a propos du Makefile:
letouzey
2007-01-12
*
un saut de ligne ...
letouzey
2007-01-12
*
addition du neq unicode
letouzey
2007-01-12
*
Petit oubli dans commit 9474
herbelin
2007-01-11
*
Ajout d'une option de débogage pour expliciter l'instance des evars
herbelin
2007-01-11
*
- Make .vo files depend on coqdoc if COQ_XML is set (bug #848)
lmamane
2007-01-10
*
Merge with Lionel Elie Mamane's private branch:
lmamane
2007-01-10
*
Merge from Lionel Elie Mamane's private branch:
lmamane
2007-01-10
*
Suite commit restructuration discharge (application du type de
herbelin
2007-01-10
*
Nouvelle approche pour le discharge modulaire
herbelin
2007-01-10
*
Subtac fixes, support for reasoning on wf defs.
msozeau
2007-01-08
*
suite de la reparation du bug 1239: apres les inds, les records et vars de types
letouzey
2007-01-05
*
Rework subtac pattern matching equalities generation.
msozeau
2007-01-02
*
Add f_equal case for 6 arguments.
msozeau
2007-01-02
*
Protection contre une source possible de liaison de lambda anonyme
herbelin
2006-12-29
*
Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à
herbelin
2006-12-28
*
Correction petits bugs du check de la test-suite
herbelin
2006-12-28
*
Remplacement de la définition de Pind et Prec par une définition
herbelin
2006-12-28
*
Cleaning backtracking code, optimized "Backtrack n x y" when n is
courtieu
2006-12-28
*
Report correction bug #1289 dans trunk (r9435 pour branche v8.1)
herbelin
2006-12-26
*
Doc for Combined Scheme.
msozeau
2006-12-23
*
Addition of a "Combined Scheme" vernacular command for building the conjuncti...
msozeau
2006-12-23
*
Default tactic for solving goals.
msozeau
2006-12-22
*
remplacement d'un test d'egalite par un test de convertibilite dans injection...
jforest
2006-12-22
*
typo malencontreuse
filliatr
2006-12-21
*
Adaptation à Subversion 1.4
notin
2006-12-19
*
reparation bug 1239
letouzey
2006-12-17
*
Changement dans ring et field, beaucoup de correction d'erreurs,
bgregoir
2006-12-15
*
contrib/dp: tactique ergo (voir ergo.lri.fr)
filliatr
2006-12-15
*
Confusion sur le paramètre à donner à concrete_name lors du commit 9450
herbelin
2006-12-14
*
Reimplemented equality generation for pattern matching at typing time. First ...
msozeau
2006-12-14
*
Alignement de la politique de renommage de rename_bound_var (utilisé pour
herbelin
2006-12-13
*
test condition de garde
barras
2006-12-13
*
svn:ignore
herbelin
2006-12-13
*
Dépliage du terme d'induction avant suppression quand celui-ci est un
herbelin
2006-12-13
*
Correction du bug #1273, deuxième version (avec des shémas d'elimination pl...
notin
2006-12-12
*
Correction du bug #1273 (problème avec les paramètres non récursivement un...
notin
2006-12-12
*
Subtac: work on cases.
msozeau
2006-12-12
*
nouvelle indentation des scripts
barras
2006-12-12
[prev]
[next]